From: Makarius <makarius@sketis.net>

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

isabelle-dev@in.tum.de

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

From: Lawrence Paulson <lp15@cam.ac.uk>

And good riddance to it!

Larry

Last updated: Sep 11 2024 at 16:22 UTC