>> On 7 Sep 2018, at 19:18, Makarius <makar...@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
Sledgehammer_Isar_Proof.
Any opinions on that?
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
