Time 
Nick 
Message 
01:51 

ilbot3 joined #isabelle 
01:51 

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/ 
04:52 

stoopkid_ joined #isabelle 
07:32 

inte joined #isabelle 
09:45 
chuchucorny 
inte: thx 
18:03 
pruvisto 
chindy: "_ > 0" seems needlessly strong 
18:03 
pruvisto 
certainly, _ ? 0" will suffice 
18:03 
pruvisto 
I'll look into it 
18:04 
pruvisto 
unless I forget 
18:04 
chindy 
good point 
18:04 
pruvisto 
in which case you can feel free to remind me ^^ 
18:04 
chindy 
:) 
18:05 
pruvisto 
chuchucorny: honestly I don't really see the point 
18:05 
pruvisto 
why set up I/O stuff in Isabelle if you can't reason about it? 
18:08 
chindy 
can someone explain why a known possibilty to derive False, does not seem to be a big enough problem to fix it? (the word64 bug in sml 5.6) 
18:09 
larsrh 
chindy: it requires custom setup to be triggered 
18:09 
larsrh 
'eval' is always prone to these problems 
18:09 
larsrh 
i.e. it is trivial you can make custom setup 
18:09 
larsrh 
err 
18:09 
larsrh 
i.e. it is trivial to make custom setup that derives 'False' 
18:10 
larsrh 
even without exploiting compiler bugs 
18:21 
chindy 
does eval work with oracles? 
18:27 
larsrh 
yep 
18:27 
larsrh 
it generates code from the current goal and checks whether that evaluates to True 
18:29 
chindy 
larsrh: i see... and the "proofs" from oracles dont go through the kernel? 
18:29 
larsrh 
nope 
18:29 
larsrh 
they only get typechecked, that's it 
18:30 
chindy 
but metis/smt/... go through the kernel, right? 
18:31 
larsrh 
yes 
21:55 
chindy 
also: http://downthetypehole.de/paste/5NJWfWkp 
21:55 
chindy 
would be nice if this could be added to GCD 