Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-05-10

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

All times shown according to UTC.

Time Nick Message
12:52 chuchucorny joined #isabelle
12:52 chuchucorny hi
12:52 chuchucorny can I increase the ML stack size somehow?
12:53 chuchucorny it seems that somewhere in Local_Theory.define or Local_Theory.note, ML runs out of stack
12:53 chuchucorny or is there a better way to get a term registered to a name binding?
13:14 fracting joined #isabelle
14:30 fracting joined #isabelle
14:33 fracting joined #isabelle
14:38 fracting joined #isabelle
15:22 fracting joined #isabelle
15:24 chuchucorny solved. solution: just do things correctly ^^
19:13 cocreature joined #isabelle
19:16 cocreature Hey, this might be a stupid question, but I have a goal that looks like P ==> (P ==> Q) ==> Q and I am trying to figure out how I can solve it using “manual” tactics (no auto, simpl, …).
19:18 cocreature find_theorems doesn’t seem to contain anything useful for that
19:19 cocreature ah I can throw conjunct1 followed by context_conjI on it
19:23 cocreature hm know than I into the same problem
19:23 cocreature s/know/no/
19:43 tautologico joined #isabelle
20:38 larsrh cocreature: are you required to solve it by a tactic invocation, or would an elementary Isar proof be fine too?
20:39 cocreature larsrh: I’m not required to, but I want to do it in different ways for learning purposes.
20:40 larsrh cocreature: I see. Sadly my lowlevel tactic-fu isn't that great
20:52 cocreature larsrh: no worries, thanks for trying to help anyway

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