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} }