Technical reports

Locales
A sectioning concept for Isabelle

Florian Kammüller, Markus Wenzel

October 1998, 16 pages

DOI: 10.48456/tr-449

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 assumptions are made, and theorems are proved which depend on these assumptions. A locale may also contain constants 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. It also discusses some implementation issues.

Full text

PDF (1.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-449,
  author =	 {Kamm{\"u}ller, Florian and Wenzel, Markus},
  title = 	 {{Locales : A sectioning concept for Isabelle}},
  year = 	 1998,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-449.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-449},
  number = 	 {UCAM-CL-TR-449}
}