Time 
Nick 
Message 
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/ 
10:02 

eng500 joined #isabelle 
18:55 

eng500 joined #isabelle 
20:01 

safinask1r joined #isabelle 
20:01 
safinask1r 
isabelle remember proof objects, i. e. full proofs, right? why? why not keep just proved facts? 
20:13 
ThreeOfEight 
Isabelle normally doesn't have proof objects. 
20:14 
ThreeOfEight 
You can run it with proof objects somehow, I think. 
20:14 
ThreeOfEight 
that is useful if you want to export proofs to other systems, as far as I know 
21:59 
safinask1r 
ThreeOfEight: but isabelle has small kernel :) and this small kernel constructs proof object. so, it follows, isabelle still keeps all proof objects, right? 
23:03 

eng500 joined #isabelle 