[isabelle-dev] Explorer.thy [was: performance problems]
Mathias.Fleury at ens-rennes.fr
Wed Sep 12 12:12:20 CEST 2018
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.
> On 12. Sep 2018, at 11:12, Lawrence Paulson <lp15 at 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.
>> 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 --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev