\documentclass{article}
\newif\ifremarks
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
\usepackage{cl2emono-modified,isabelle,isabellesym}
\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
\usepackage{../proof,amsmath}
\usepackage{../pdfsetup} %last package!
%\newtheorem{theorem}{Theorem}[section]
\newtheorem{Exercise}{Exercise}[section]
\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
\newcommand{\ttlbr}{\texttt{[|}}
\newcommand{\ttrbr}{\texttt{|]}}
\newcommand{\ttor}{\texttt{|}}
\newcommand{\ttall}{\texttt{!}}
\newcommand{\ttuniquex}{\texttt{?!}}
\newcommand{\ttEXU}{\texttt{EX!}}
\newcommand{\ttAnd}{\texttt{!!}}
\newcommand{\isasymimp}{\isasymlongrightarrow}
\newcommand{\isasymImp}{\isasymLongrightarrow}
\newcommand{\isasymFun}{\isasymRightarrow}
\newcommand{\isasymuniqex}{\isamath{\exists!\,}}
\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
%% lcp's macros
\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
\newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
\let\bigisa=\isa
%% was previously
%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}}
%% because \isa is too small for variables, but does it really matter?
%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
%% run ../sedindex logics to prepare index file
\makeindex
\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
\index{product type|see{pair}}
\index{tuple|see{pair}}
\underscoreoff
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
\pagestyle{headings}
%\sloppy
%\binperiod %%%treat . like a binary operator
\begin{document}
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
Technische Universit{\"a}t M{\"u}nchen \\
Institut f{\"u}r Informatik \\[1ex]
University of Cambridge\\
Computer Laboratory}
\maketitle
\pagenumbering{roman}
\tableofcontents
\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Olaf M{\"u}ller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
read and comment on a draft version.
\clearfirst
\input{basics}
\input{fp}
\input{Rules/rules}
\input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
\input{Inductive/inductive}
\input{Advanced/advanced}
\input{Types/types}
\chapter{Theory Presentation}
\chapter{Case Study: The Needhamd-Schroeder Protocol}
\chapter{Structured Proofs}
\chapter{Case Study: UNIX File-System Security}
%\chapter{The Tricks of the Trade}
\input{appendix}
\bibliographystyle{plain}
\bibliography{../manual}
\printindex
\end{document}