Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-03-18

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

All times shown according to UTC.

Time Nick Message
05:31 fracting joined #isabelle
10:11 int-e is there a way to give the intro rule that results from using "obtains" a name?
10:12 int-e (this syntax:  lemma obtains foo where blah)
10:13 int-e oh it's called "that", hmm
10:16 larsrh int-e: I can only guess that that's some inside joke :-)
10:16 larsrh So you can write 'from this and that have ...'
10:17 int-e using that by blast <-- yeah it looks silly
10:20 int-e section 2.2.2 in isar-ref should probably mention "that".
11:50 ThreeOfEight this is also the default name given to assumptions introduced by "if"
11:50 ThreeOfEight and by this I mean "that"
12:29 Damaki joined #isabelle
13:10 int-e good to know
13:23 larsrh ThreeOfEight: could you solve your attribute problem?
14:43 Damaki joined #isabelle
14:57 ThreeOfEight larsrh: havent tried yet
15:30 fracting joined #isabelle
16:08 fracting joined #isabelle
21:26 chuchucorny joined #isabelle

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