Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01: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/ 
02:03 

fracting joined #isabelle 
02:26 

fracting joined #isabelle 
04:31 

fracting joined #isabelle 
05:00 

fracting joined #isabelle 
06:18 

kyagrd joined #isabelle 
11:04 

fracting joined #isabelle 
11:37 

fracting joined #isabelle 
12:03 

fracting joined #isabelle 
12:39 

fracting joined #isabelle 
13:36 

silver joined #isabelle 
18:33 
chuchucorny 
I just heared there is a quickcheck (as in haskell quickcheck) for ML. Is this available in Isabelle/ML? 
19:54 
larsrh 
it's called Spec_Check 
19:55 
larsrh 
you can find it in the distribution 
19:56 
cocreature 
is there a way to refer to the induction hypothesis when my cases don’t have names? I’m doing induction using the induction rule of a fun and the hypothesis is fairly long so I’d like to avoid having to type the whole thing 
19:59 
inte 
if you have case (1 x y), then the 1 is a case name and you can refer to the induction hypothesis as 1. 
19:59 
inte 
(in my experience) 
19:59 
cocreature 
inte: ah great that works! I was trying 1.IH like Case.IH and that doesn’t do the trick 
20:05 
inte 
cocreature: oh. you need quotes for that... "1.IH" works. 
20:05 
cocreature 
inte: ah I tried "1".IH :) 
23:47 

fracting joined #isabelle 