Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-04-02

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

All times shown according to UTC.

Time Nick Message
07:26 fracting joined #isabelle
15:52 Damaki joined #isabelle
21:13 JCaesar There's no neat trick that would invoke sledgehammer on all sorrys I have in my text selection and insert the proof if it finds one?
21:18 int-e not that I know of. the different but similar question https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00053.html didn't get any suggestions
21:39 larsrh int-e: I don't think this question is similar; it talks about one specific statement
21:39 larsrh JCaesar: There's "Judgement day"
21:40 larsrh I think ultimately you can call this via "isabelle mirabelle"
21:41 int-e larsrh: It's at least superficially similar in that it is about invoking sledgehammer on several goals...
21:41 larsrh although I'm not sure how well that works in practice
22:35 fracting1 joined #isabelle

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