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.
- Projects
- None
- Subscribers
- None