Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-02-28

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

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

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary