<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">This looks interesting and useful. I
think the command should take a method as input and apply it, i.e.<br>
<br>
explore meth<br>
<br>
will result in<br>
<br>
proof meth<br>
...<br>
qed<br>
<br>
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.<br>
<br>
Dmitriy<br>
<br>
Am 18.08.2013 16:39, schrieb Florian Haftmann:<br>
</div>
<blockquote cite="mid:5210DCA3.5060005@informatik.tu-muenchen.de"
type="cite">
<pre wrap="">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
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>