[isabelle-dev] Explorer.thy [was: performance problems]
lp15 at cam.ac.uk
Wed Sep 12 11:12:13 CEST 2018
I regard it as indispensable. But it does need better pretty printing. Also I greatly prefer the if/for format to assume/fix.
> On 12 Sep 2018, at 07:23, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>> On 7 Sep 2018, at 19:18, Makarius <makarius at sketis.net> wrote:
>>> I can't try it out, since theory "Explorer" is missing.
>> Attached. A very cool thing.
> Nice to see that old draft from 5 years ago.
> I would still agree that such a tool would be tremendously useful, but
> before going into the distro it would need technical improvement, i.e.
> more civilized approach toward Isar proof text generation, similar to
> Any opinions on that?
> PGP available:
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: Message signed with OpenPGP
More information about the isabelle-dev