27 \author{Clemens Ballarin} |
27 \author{Clemens Ballarin} |
28 \date{} |
28 \date{} |
29 |
29 |
30 \maketitle |
30 \maketitle |
31 |
31 |
32 %\thispagestyle{myheadings} |
|
33 %\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007} |
|
34 \thispagestyle{myheadings} |
|
35 \markright{This tutorial is currently not consistent.} |
|
36 |
|
37 \begin{abstract} |
32 \begin{abstract} |
38 Locales are Isabelle's mechanism to deal with parametric theories. |
33 Locales are Isabelle's mechanism for dealing with parametric theories. |
39 We present typical examples of locale specifications, |
34 We present typical examples of locale specifications, |
40 along with interpretations between locales to change their |
35 along with interpretations between locales to change their |
41 hierarchic dependencies and interpretations to reuse locales in |
36 hierarchic dependencies and interpretations to reuse locales in |
42 theory contexts and proofs. |
37 theory contexts and proofs. |
43 |
38 |
44 This tutorial is intended for locale novices; familiarity with |
39 This tutorial is intended for locale novices; familiarity with |
45 Isabelle and Isar is presumed. |
40 Isabelle and Isar is presumed. |
46 The 2nd revision accommodates changes introduced by the locales |
41 The second revision accommodates changes introduced by the locales |
47 reimplementation for Isabelle 2009. Most notably, in complex |
42 reimplementation for Isabelle 2009. Most notably, in complex |
48 specifications (\emph{locale expressions}) renaming has been |
43 specifications (\emph{locale expressions}) renaming has been |
49 generalised to instantiation. |
44 generalised to instantiation. |
50 \end{abstract} |
45 \end{abstract} |
51 |
46 |