<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">Hi all,</div><div class=""><br class=""></div><div class=""><br class=""></div>I have my own version of explore (<a href="https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy" class="">https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy</a>), which does not have better pretty printing, but has two variants that I find indispensable: explore_have produces "have … if … for …" and explore_lemma produces "lemma fixes … assumes … shows …". There is even an option for cartouches.<div class=""><br class=""></div><div class=""><br class=""><div><br class=""></div><div>Mathias</div><div><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">On 12. Sep 2018, at 11:12, Lawrence Paulson <<a href="mailto:lp15@cam.ac.uk" class="">lp15@cam.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class=""><div class="protected-part"><div class="protected-title">Signed PGP part</div><div class="protected-content">I regard it as indispensable. But it does need better pretty printing. Also I greatly prefer the if/for format to assume/fix.</div></div></div></div></blockquote><blockquote type="cite" class=""><div class=""><div class=""><div class="protected-part"><div class="protected-content"><br class="">Larry<br class=""><br class=""><blockquote type="cite" class="">On 12 Sep 2018, at 07:23, Florian Haftmann <<a href="mailto:florian.haftmann@informatik.tu-muenchen.de" class="">florian.haftmann@informatik.tu-muenchen.de</a>> wrote:<br class=""><br class=""><blockquote type="cite" class=""><blockquote type="cite" class="">On 7 Sep 2018, at 19:18, Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>> wrote:<br class=""><br class="">I can't try it out, since theory "Explorer" is missing.<br class=""></blockquote><br class="">Attached. A very cool thing.<br class=""></blockquote><br class="">Nice to see that old draft from 5 years ago.<br class=""><br class="">I would still agree that such a tool would be tremendously useful, but<br class="">before going into the distro it would need technical improvement, i.e.<br class="">more civilized approach toward Isar proof text generation, similar to<br class="">Sledgehammer_Isar_Proof.<br class=""><br class="">Any opinions on that?<br class=""><br class="">Cheers,<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Florian<br class=""><br class="">--<br class=""><br class="">PGP available:<br class=""><a href="http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de" class="">http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de</a><br class=""><br class=""></blockquote><br class=""></div></div><br class=""><iframe class="untrusted-content-test" scrolling="auto" width="200" height="20" style="border:none;display:block;overflow:auto;" data-src="data:text/html;charset=UTF-8;base64,PGlmcmFtZS1jb250ZW50Pl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fPEJSPmlzYWJlbGxlLWRldiBtYWlsaW5nIGxpc3Q8QlI+aXNhYmVsbGUtZGV2QGluLnR1bS5kZTxCUj5odHRwczovL21haWxtYW5icm95LmluZm9ybWF0aWsudHUtbXVlbmNoZW4uZGUvbWFpbG1hbi9saXN0aW5mby9pc2FiZWxsZS1kZXY8QlI+PC9pZnJhbWUtY29udGVudD4=" sandbox="allow-scripts"></iframe></div></div></blockquote></div><br class=""></div></body></html>