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

[Lawrence Paulson]

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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180912/c372552b/attachment.sig>