doc-src/Locales/Locales/document/root.tex
 author wenzelm Wed, 04 Jun 2008 17:12:00 +0200 changeset 27082 9102d87efd3d parent 27078 41483ec1b5b6 child 29566 937baa077df2 permissions -rw-r--r--
tikz: change to pgfsys-dvi.def for plain dvi output;

\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}

\isafoldtag{proof}

% urls in roman style, theory text in typewriter
\urlstyle{rm}
\isabellestyle{tt}

\begin{document}

\title{Tutorial to Locales and Locale Interpretation}
\author{Clemens Ballarin}
\date{}

\maketitle

\markright{Technical Report TUM-I0723, Technische Universit\"at M\"unchen, 2007}

\begin{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.
\end{abstract}

\parindent 0pt\parskip 0.5ex

\input{session}

\newpage
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: