CODEWITHSUNDEEP
isabelle
Wolfgang Jeltsch
Wolfgang Jeltsch

Reputation: 801

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.

Upvotes: 2

Views: 134

Answers (1)

chris
chris

Reputation: 5018

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.

Upvotes: 3

Related Questions