And good riddance to it! Larry On 27 Sep 2021, 16:17 +0100, Makarius <[email protected]>, wrote: *** Isar ***
* The improper proof command 'guess' is no longer part of by Pure, but provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY, existing applications need to import session "Pure-ex" and theory "Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess' command, using explicit 'obtain' instead. This refers to Isabelle/b49bd5d9041f and AFP/2056abab0dd6. The AFP changeset is representative for the kind of (non-)applications of 'guess'. It originally stems from a discussion about improper Isar add-ons in 2006. In the 10 years later so many better ways to mix structured and unstructured proofs emerged, e.g. the 'subgoal' command. So today, there would be no point to introduce such a command at all. In the above AFP change, I have either turned the non-Isar "wild guesses" into proper 'obtain', or rephrased the proofs slightly to avoid the awkward situation in the first place. In a few cases, left things unchanged and did import "Pure-ex.Guess" as explained above. This is in contrast to the Isabelle distribution where all guesses within Isar proofs are already gone --- mostly derived from Robert Himmelmann's initial work on HOL-Analysis n years ago. Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
