[isabelle-dev] Draft toy for proof exploration
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.
will result in
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,
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev