
<html xmlns="http://www.w3.org/1999/xhtml">


<head>


<meta http-equiv="Content-Type" content="text/html; charset=utf-8">


<title></title>


</head>


<body>


<div name="messageBodySection">


<div dir="auto">And good riddance to it!</div>


</div>


<div name="messageSignatureSection"><br>


<div class="matchFont">


<div dir="auto">Larry</div>


</div>


</div>


<div name="messageReplySection">On 27 Sep 2021, 16:17 +0100, Makarius <makarius@sketis.net>, wrote:<br>


<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">


*** Isar ***<br>


<br>


* The improper proof command 'guess' is no longer part of by Pure, but<br>


provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY,<br>


existing applications need to import session "Pure-ex" and theory<br>


"Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess'<br>


command, using explicit 'obtain' instead.<br>


<br>


<br>


This refers to Isabelle/b49bd5d9041f and AFP/2056abab0dd6. The AFP changeset<br>


is representative for the kind of (non-)applications of 'guess'. It originally<br>


stems from a discussion about improper Isar add-ons in 2006. In the 10 years<br>


later so many better ways to mix structured and unstructured proofs emerged,<br>


e.g. the 'subgoal' command. So today, there would be no point to introduce<br>


such a command at all.<br>


<br>


In the above AFP change, I have either turned the non-Isar "wild guesses" into<br>


proper 'obtain', or rephrased the proofs slightly to avoid the awkward<br>


situation in the first place. In a few cases, left things unchanged and did<br>


import "Pure-ex.Guess" as explained above.<br>


<br>


This is in contrast to the Isabelle distribution where all guesses within Isar<br>


proofs are already gone --- mostly derived from Robert Himmelmann's initial<br>


work on HOL-Analysis n years ago.<br>


<br>


<br>


Makarius<br>


_______________________________________________<br>


isabelle-dev mailing list<br>


isabelle-dev@in.tum.de<br>


https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br>


</blockquote>


</div>


</body>


</html>