Locales a sectioning concept for Isabelle
F Kammüller, M Wenzel, LC Paulson - … ' 99 Nice, France, September 14–17 …, 1999 - Springer
F Kammüller, M Wenzel, LC Paulson
Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs …, 1999•SpringerLocales are a means to define local scopes for the interactive proving process of the
theorem prover Isabelle. They delimit a range in which fixed assumption are made, and
theorems are proved that depend on these assumptions. A locale may also contain
constants defined locally and associated with pretty printing syntax. Locales can be seen as
a simple form of modules. They are similar to sections as in AUTOMATH or Coq. Locales are
used to enhance abstract reasoning and similar applications of theorem provers. This paper …
theorem prover Isabelle. They delimit a range in which fixed assumption are made, and
theorems are proved that depend on these assumptions. A locale may also contain
constants defined locally and associated with pretty printing syntax. Locales can be seen as
a simple form of modules. They are similar to sections as in AUTOMATH or Coq. Locales are
used to enhance abstract reasoning and similar applications of theorem provers. This paper …
Abstract
Locales are a means to define local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants defined locally and associated with pretty printing syntax.
Locales can be seen as a simple form of modules. They are similar to sections as in AUTOMATH or Coq. Locales are used to enhance abstract reasoning and similar applications of theorem provers. This paper motivates the concept of locales by examples from abstract algebraic reasoning. It also discusses some implementation issues.
Springer