Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-08-31

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

All times shown according to UTC.

Time Nick Message
01:07 Warrigal_ joined #isabelle
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/
02:56 hazyPurple joined #isabelle
04:34 hazyPurple joined #isabelle
05:08 hazyPurple joined #isabelle
10:11 aindilis joined #isabelle
10:34 aindilis joined #isabelle
12:49 chindy http://downthetypehole.de/paste/QHiQ6QIO why does the upper proof work but the lower does not ?
12:49 chindy the difference is that line 7/8 are two lines below
13:46 hazyPurple joined #isabelle
14:47 hazyPurple joined #isabelle
20:59 int-e What does "does not work" mean here? Does any proof step fail? The qed will fail because of the duplicate lemma name.
23:34 Warrigal_ joined #isabelle

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