Tutorial to Locales and Locale Interpretation

Document type:: Technical Report
Author(s):: Clemens Ballarin
Title:: Tutorial to Locales and Locale Interpretation
Abstract:: Locales are Isabelle's mechanism to deal with parametric theories. We present typical examples of locale specifications, along with interpretations between locales to change their hierarchic dependencies and interpretations to reuse locales in theory contexts and proofs.\\ This tutorial is intended for locale novices; familiarity with Isabelle and Isar is presumed.
Keywords:: Interactive proof; theory interpretation; Isabelle
Year:: 2007
Year / month:: 2007-12-01 00:00:00
Pages:: 17
BibTeX

Occurrences: