I regard it as indispensable. But it does need better pretty printing. Also I greatly prefer the if/for format to assume/fix.
Larry > On 12 Sep 2018, at 07:23, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > >>> 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: Message signed with OpenPGP
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
