[isabelle-dev] Draft toy for proof exploration

Dmitriy Traytel traytel at in.tum.de
Mon Aug 19 09:49:42 CEST 2013

This looks interesting and useful. I think the command should take a 
method as input and apply it, i.e.

explore meth

will result in

proof meth

However when writing this, I notice that rather than "explore", I want 
to use a plain "apply" and have a button/pop-up "Isarify state" shown 


Am 18.08.2013 16:39, schrieb Florian Haftmann:
> Hello all,
> find attached a draft theory which establishes an experimental »explore«
> command which prints a goal state as Isar statement within the theory.
> It is merely meant as a starting point for discussion and
> experimentation. A first step would be a proper abstract printable
> representation of Isar statements. Maybe the sledgehammer gurus have
> further ideas about that!?
> Happy hacking,
> 	Florian
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

More information about the isabelle-dev mailing list