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 prepackaged 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/tests/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 