Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-28

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

All times shown according to UTC.

Time Nick Message
01:52 ilbot3 joined #isabelle
01:52 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:21 wagle joined #isabelle
06:26 ammbauer In a recent discussion on the mailing list this tool (Explorer.thy) was mentioned. I wanted to try it out but I can't get it to work in 2016-1 (Error message: Undefined ML antiquotation: "command_spec"). Can anybody help me out?
06:26 ammbauer Link: https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04443.html
06:30 larsrh command_spec ~> command_keyword
06:31 pruvisto larsrh: btw, Peter called you "Manuel" again yesterday
06:31 pruvisto while talking to me even
06:32 larsrh lol
06:33 ammbauer larsrh: that leads to even more errors :|
07:45 lispy joined #isabelle
10:49 ammbauer joined #isabelle
14:27 chindy is there a way to make defintions/abbreviations private to a locale?
14:48 silver joined #isabelle
15:05 pruvisto just do "private definition"?
15:07 larsrh that requires an extra unnamed context around IIRC
15:51 chindy larsrh: yea
15:56 pruvisto oh right
20:27 ski joined #isabelle
20:28 g0d355__ joined #isabelle
23:55 silver_ joined #isabelle

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