Hi all,
I have my own version of explore (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy <https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy>), which does not have better pretty printing, but has two variants that I find indispensable: explore_have produces "have … if … for …" and explore_lemma produces "lemma fixes … assumes … shows …". There is even an option for cartouches. Mathias > On 12. Sep 2018, at 11:12, Lawrence Paulson <l...@cam.ac.uk> wrote: > > Signed PGP part > 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 >> > >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
