Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-02-03

| 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/
06:02 aindilis2 joined #isabelle
08:19 ammbauer i wanted to play around with eisbach and I can't even get the example in 1.1 <http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/eisbach.pdf> to run.
08:19 ammbauer <Outer syntax error⌂: command expected, but identifier method⌂ was found>
08:35 pruvisto ammbauer: that looks like you didn't import Eisbach
08:35 pruvisto so Isabelle doesn't even know the "method" command
08:35 pruvisto (I really should learn Eisbach some time as well; I still write ML code for everything)
08:35 pruvisto (although I suspect much of what I need is beyond the scope of Eisbach)
08:38 ammbauer imports Main "~~/src/HOL/Eisbach/Eisbach_Tools"
08:39 pruvisto what Isabelle version?
08:39 ammbauer 2016-1
08:39 ammbauer oh, sorry. It works with that imports line.
08:40 ammbauer It just isn't mentioned anywhere what to import.
08:45 pruvisto perhaps you ought to say this on the mailing list
10:27 silver joined #isabelle
11:35 JCaesar you need to import something for eisbach? *sob*
11:38 ammbauer maybe "imports Isar" works. Since the Eisbach flows into the Isar :D
11:39 JCaesar O_O
11:59 juls joined #isabelle
13:12 larsrh imports Donau
13:13 larsrh imports Black_Sea
13:33 pruvisto You are all horrible people.
14:11 JCaesar Speaking of the devil…
14:11 JCaesar Hm, nein, das ist nicht das richtige Sprichwort. Eher "Das sagt der Richtige".
14:12 int-e look who's talking
14:15 JCaesar oh, right…
17:56 mal`` joined #isabelle
19:45 dmiles joined #isabelle

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