Improper proof command 'guess' provided by separate theory "Pure-ex.Guess"
- 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.
Written by makarius on Sep 27 2021, 5:00 PM.