Fixed proof term bug in permute_prems.
\documentclass{article}
\usepackage{cl2emono-modified,isabelle,isabellesym}
\usepackage{../proof,amsmath,amsfonts}
\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
\usepackage{../pdfsetup}
%last package!
\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
%\remarksfalse
\makeindex
\index{conditional expressions|see{\isa{if} expressions}}
\index{primitive recursion|see{recursion, primitive}}
\index{product type|see{pairs and tuples}}
\index{structural induction|see{induction, structural}}
\index{termination|see{functions, total}}
\index{tuples|see{pairs and tuples}}
\index{settings|see{flags}}
\index{*<*lex*>|see{lexicographic product}}
\underscoreoff
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
\pagestyle{headings}
\begin{document}
\title{\includegraphics[scale=.8]{isabelle_hol}
\\ \vspace{0.5cm} The Tutorial
\\ --- DRAFT ---}
\author{Tobias Nipkow and Lawrence C. Paulson\\[1ex]
Technische Universit{\"a}t M{\"u}nchen \\
Institut f{\"u}r Informatik \\[1ex]
University of Cambridge\\
Computer Laboratory}
\maketitle
\pagenumbering{roman}
\setcounter{page}{5}
\vspace*{\fill}
\begin{center}
\LARGE In memoriam \\[1ex]
{\sc Annette Schumann}\\[1ex]
1959 -- 2001
\end{center}
\vspace*{\fill}
\vspace*{\fill}
\newpage
\input{preface}
\tableofcontents
\cleardoublepage\pagenumbering{arabic}
\input{basics}
\input{fp}
\input{Rules/rules}
\input{Sets/sets}\input{CTL/ctl} %these constitute ONE chapter
\input{Inductive/inductive}
\input{Types/types}
\input{Advanced/advanced}
%\chapter{Theory Presentation} Document preparation / Syntax Matters!
\input{Protocol/protocol}
%\chapter{Structured Proofs}
%\label{ch:Isar}
%\chapter{Case Study: UNIX File-System Security}
%\chapter{The Tricks of the Trade}
\input{appendix}
\bibliographystyle{plain}
\bibliography{../manual}
\printindex
\end{document}