Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-05-25

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

All times shown according to UTC.

Time Nick Message
00:41 tautologico joined #isabelle
00:58 fracting joined #isabelle
01:30 fracting joined #isabelle
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/
03:22 fracting joined #isabelle
04:26 fracting joined #isabelle
06:51 fracting joined #isabelle
08:22 fracting joined #isabelle
09:50 ammbauer joined #isabelle
09:50 ammbauer ThreeOfEight: is "proof (clarsimp)" okay to use?
09:51 larsrh ammbauer: no
09:52 ThreeOfEight ammbauer: my personal policy is: using the simplifier in the initial method of a "proof" is only admissible with an "only: " simpset
09:53 ThreeOfEight and even then it is somewhat undesirable
09:55 chuchucorny /cc JCaesar
10:46 JCaesar chuchucorny: I am perfectly aware of that.
10:54 fracting joined #isabelle
11:13 cocreature joined #isabelle
11:19 ski joined #isabelle
12:26 fracting joined #isabelle
12:39 fracting joined #isabelle
12:56 fracting joined #isabelle
13:20 cocreature joined #isabelle
22:04 Damaki joined #isabelle
23:30 tautologico joined #isabelle

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