[isabelle-dev] Explorer.thy [was: performance problems]

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Sep 12 08:23:20 CEST 2018

>> 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...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180912/510a73ba/attachment.sig>

More information about the isabelle-dev mailing list