Front matter updated.
\documentclass[11pt,a4paper]{article}
\usepackage{amsmath}
\usepackage{ifpdf}
\ifpdf\relax\else\def\pgfsysdriver{pgfsys-dvi.def}\fi
\usepackage{tikz}
\usepackage{subfigure}
\usepackage{../../../isabelle,../../../isabellesym}
\usepackage{verbatim}
\usepackage{array}
\usepackage{amssymb}
\usepackage{../../../pdfsetup}
\isadroptag{theory}
\isafoldtag{proof}
% urls in roman style, theory text in typewriter
\urlstyle{rm}
\isabellestyle{tt}
\begin{document}
\title{Tutorial to Locales and Locale Interpretation \\[1ex]
\large 2nd revision, for Isabelle 2009}
\author{Clemens Ballarin}
\date{}
\maketitle
\begin{abstract}
Locales are Isabelle's mechanism for dealing 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.
The second revision accommodates changes introduced by the locales
reimplementation for Isabelle 2009. Most notably, in complex
specifications (\emph{locale expressions}) renaming has been
generalised to instantiation.
\end{abstract}
\parindent 0pt\parskip 0.5ex
\input{session}
\newpage
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: