HomeIsabelle/Phabricator
Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"

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.

Written by makarius on Sep 27 2021, 5:00 PM.
User
Projects
None
Subscribers
None

Event Timeline