Time 
Nick 
Message 
00:40 

wagle joined #isabelle 
00:54 

wagle joined #isabelle 
01:46 

wagle joined #isabelle 
02:24 

wagle joined #isabelle 
02:48 

ilbot3 joined #isabelle 
02:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
11:01 

silver joined #isabelle 
11:31 
JCaesar 
I just accidentally wrote unfolding _foo_def instead of unfolding foo_defâ€¦ and that still works? wtf? 
11:56 
inte 
seems to be some auxilliary theorem produced by "definition". 
11:59 
inte 
(I have no clue why) 
12:05 
larsrh 
name bindings starting with _ are supposed to be deprecated iirc 
12:05 
larsrh 
well, "legacy" in Isabelle parlance 
12:06 
inte 
I'm curious though, the _foo_def comes with a PROP ?psi ==> PROP ?psi, what is that part about? 
12:07 
inte 
(it doesn't appear to have anything to do with locales) 
12:07 
inte 
And it probably doesn't matter, really. But it's odd. 
12:07 
larsrh 
heh, we all got confused by tokenization 
12:07 
larsrh 
I just tried it 
12:08 
larsrh 
thm _foo_def gets tokenized as thm, _, foo_def 
12:08 
larsrh 
_ is in fact the PROP ?psi ==> PROP ?psi theorem 
12:08 
inte 
oh. ouch. 
12:08 
larsrh 
it's the same one you use for partial theorem application: using foobar[OF _ meep] 
12:08 
inte 
thanks! 
12:08 
larsrh 
OTOH, thm "_foo_def" leads to "undefined fact" 
12:08 
inte 
I always thought that was syntax... 
12:09 
larsrh 
no, it's registered somewhere deep down in Isar/Pure 
12:10 
inte 
so it's a bit like "otherwise" in Haskell :) 
12:10 
larsrh 
exactly :) 
13:25 
JCaesar 
heh. 