Search code examples
isabelle

Isabelle 2017: Support for proof method definitons seems to be lacking

Isabelle is supposed to come with Eisbach, a language for easily defining your own proof methods. The Isabelle/jEdit IDE has a link to the Eisbach User Manual, but Eisbach seems to be unavailable. The token methods is treated as an identifier by the IDE’s syntax checker, and auto-completion does not know about a methods keyword either.

How can I access Eisbach? Do method definitions have to go into special files instead of theory files? At least, I did not find anything in the Eisbach User Manual that said so.

Solution

  • The documentation seems to miss (at least I couldn't find a hint) that you have to import the Eisbach theory in addition to Main

    theory My_Theory
  import
    Main
    "HOL-Eisbach.Eisbach"
begin

    before Eisbach is available inside your theory file.