[isabelle-dev] Draft toy for proof exploration

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Aug 18 16:39:31 CEST 2013

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,


PGP available:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Explorer.thy
Type: application/x-extension-thy
Size: 1802 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130818/558a92e7/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130818/558a92e7/attachment.asc>

More information about the isabelle-dev mailing list