Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-08-11

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

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #isabelle
01:47 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:45 dmiles joined #isabelle
05:46 chuchuco1ny joined #isabelle
05:49 ThreeOfEight larsrh: but then you have to chain in /only/ the facts that the rule requires and in the right order
05:54 kini joined #isabelle
06:18 larsrh ThreeOfEight: yes
06:18 larsrh but if you're using apply - apply (erule ... ) your assumptions better be in the right order too
06:22 ThreeOfEight Only if there are multiple possibilities
06:22 ThreeOfEight Otherwise, it shouldn't matter. Should it?
06:28 larsrh if they're in the wrong order you need to slap an '; assumption' at the end
06:48 ThreeOfEight ah I see
06:48 ThreeOfEight or use "by"
09:22 dmiles joined #isabelle
09:44 silver joined #isabelle
12:49 Damaki joined #isabelle
14:16 silver_ joined #isabelle

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