[isabelle] New locales tutorial available

A new locales tutorial (for Isabelle 2007) is now available:

Clemens Ballarin. Tutorial to Locales and Locale Interpretation. Technical Report TUM-I0723, Technische Universität München, 2007.


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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.