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

[Mathias Fleury]

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 <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.
> 
> Larry
> 
>> 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
>> 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
>> 
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180912/da44c309/attachment-0002.html>