[isabelle-dev] Draft toy for proof exploration

[Dmitriy Traytel]

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

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

Dmitriy

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>