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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
