Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Improper proof command 'guess' provi...


view this post on Zulip Email Gateway (Sep 27 2021 at 15:17):

From: Makarius <makarius@sketis.net>
* Isar *

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

view this post on Zulip Email Gateway (Sep 27 2021 at 15:23):

From: Lawrence Paulson <lp15@cam.ac.uk>
And good riddance to it!

Larry


Last updated: Mar 04 2024 at 10:08 UTC