[isabelle-dev] Draft toy for proof exploration

[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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- 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>