1\documentclass[11pt,a4paper]{article}
2\usepackage{lmodern}
3\usepackage[T1]{fontenc}
4\usepackage{tikz}
5\usepackage{subfigure}
6\usepackage[nohyphen,strings]{underscore}
7\usepackage{amsmath}
8\usepackage{isabelle,isabellesym}
9\usepackage{verbatim}
10\usepackage{alltt}
11\usepackage{array}
12
13\usepackage{amssymb}
14
15\usepackage{pdfsetup}
16
17\isadroptag{theory}
18\isafoldtag{proof}
19
20% urls in roman style, theory text in typewriter
21\urlstyle{rm}
22\isabellestyle{tt}
23
24
25\begin{document}
26
27\title{Tutorial to Locales and Locale Interpretation%
28\thanks{Published in L.~Lamb\'an, A.~Romero, J.~Rubio, editors, {\em Contribuciones Cient\'{\i}ficas en honor de Mirian Andr\'es.}  Servicio de Publicaciones de la Universidad de La Rioja, Logro\~no, Spain, 2010.  Reproduced by permission.}}
29\author{Clemens Ballarin}
30\date{}
31
32\maketitle
33
34\begin{abstract}
35  Locales are Isabelle's approach for dealing with parametric
36  theories.  They have been designed as a module system for a
37  theorem prover that can adequately represent the complex
38  inter-dependencies between structures found in abstract algebra, but
39  have proven fruitful also in other applications --- for example,
40  software verification.
41
42  Both design and implementation of locales have evolved considerably
43  since Kamm\"uller did his initial experiments.  Today, locales
44  are a simple yet powerful extension of the Isar proof language.
45  The present tutorial covers all major facilities of locales.  It is
46  intended for locale novices; familiarity with Isabelle and Isar is
47  presumed.
48\end{abstract}
49
50\parindent 0pt\parskip 0.5ex
51
52\input{session}
53
54\bibliographystyle{abbrv}
55\bibliography{root}
56
57\end{document}
58
59%%% Local Variables:
60%%% mode: latex
61%%% TeX-master: t
62%%% End:
63