use isabelle style files from Doc/ -- not the generated ones (which are not present in the repository anyway);
\documentclass[11pt,a4paper]{article}
\usepackage{amsmath}
\usepackage{tikz}
\usepackage{subfigure}
\usepackage{../isabelle,../isabellesym}
\usepackage{verbatim}
\usepackage{array}
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
\usepackage{amssymb}
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel}
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
%\usepackage[latin1]{inputenc}
%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
%\<threesuperior>, \<threequarters>, \<degree>
%\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<cent>, \<currency>
% this should be the last package used
\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
\thispagestyle{myheadings}
\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
% generated text of all theories
\input{session}
% optional bibliography
\newpage
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: