# IRC log for #isabelle, 2012-09-20

All times shown according to UTC.

Time Nick Message
02:09 Jafet joined #isabelle
03:31 Jafet joined #isabelle
10:22 gienah joined #isabelle
12:45 felipealmeida joined #isabelle
12:45 felipealmeida joined #isabelle
14:33 Muon joined #isabelle
14:33 Muon hello
14:36 Muon I want to prove some things about formulas involving floating point arithmetic, and I'm trying to use the pre-packaged Float theory
14:36 Muon however, it seems to be convinced that things specified to be float are in fact real
14:37 Muon or at least it does in the subgoals
14:41 Muon could there be another reason the first subgoal specifies reals instead of floats?
15:00 tomprince joined #isabelle
17:12 felipealmeida joined #isabelle
19:17 ChanServ joined #isabelle
19:25 felipealmeida joined #isabelle
21:06 felipealmeida joined #isabelle
21:29 mceier joined #isabelle
21:56 mceier hi, why this fails to parse at \<and> : lemma "(m \<in> Even \<Longrightarrow> 2 dvd m) \<and> (n \<in> Odd \<Longrightarrow> 2 dvd (Suc n))" ?
21:56 mceier it's from page 134 of tutorial - I entered prolog ("theory ... "), definition of inductive set, this lemma, apply rule, and epilog, but proof general fails to parse the lemma.
21:57 gienah mceier: it can get confused by comments that follow the stuff you are wanting it to parse, not sure if that is the problem here or not though
21:58 * gienah tries it
21:59 mceier hmm, I can paste the code on pastebin... if you want ;)
21:59 mceier http://pastebin.com/0KC02AtQ
22:01 gienah mceier: one possible workaround is to change the meta implications to just normal implications -->
22:03 mceier That helped, now I get error: Illegal application of proof command in "prove" mode
22:04 mceier *** At command "end" (line 17 of "/home/mceier/development/tes​ts/isabelle/first/first.thy")
22:04 gienah mceier: oh, and that is the difference between what you have and lemma on p. 134
22:05 mceier I removed "end" and it seems to work :)
22:05 mceier gienah: thanks ;)
22:06 gienah mceier: isabelle has 2 modes: (1) Isar mode if you start the proof with: proof (2) apply mode if you dont or start it with: apply -
22:06 gienah mceier: they are confusingly quite different
22:06 mceier ok, I will remember this
22:22 * gienah has to go out for about 8 hours or so
23:29 lazard joined #isabelle