[isabelle-dev] NEWS: Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"

[Makarius]

*** 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