--- a/doc-src/TutorialI/tutorial.tex Tue Aug 28 13:15:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-\documentclass{article}
-%%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters
-\usepackage{cl2emono-modified,../../lib/texinputs/isabelle,../../lib/texinputs/isabellesym}
-\usepackage{../proof,amsmath,amsfonts}
-\usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
-\usepackage{eurosym}
-\usepackage[english]{babel}
-\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{*<*lex*>|see{lexicographic product}}
-
-\underscoreoff
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
-
-\pagestyle{headings}
-
-
-\begin{document}
-\title{
-\begin{center}
-\includegraphics[scale=.8]{isabelle_hol}
- \\ \vspace{0.5cm} A Proof Assistant for Higher-Order Logic
-\end{center}}
-\author{Tobias Nipkow \quad Lawrence C. Paulson \quad Markus Wenzel%\\[1ex]
-%Technische Universit{\"a}t M{\"u}nchen \\
-%Institut f{\"u}r Informatik \\[1ex]
-%University of Cambridge\\
-%Computer Laboratory
-}
-\pagenumbering{roman}
-\maketitle
-\newpage
-
-%\setcounter{page}{5}
-%\vspace*{\fill}
-%\begin{center}
-%\LARGE In memoriam \\[1ex]
-%{\sc Annette Schumann}\\[1ex]
-%1959 -- 2001
-%\end{center}
-%\vspace*{\fill}
-%\vspace*{\fill}
-%\newpage
-
-\include{preface}
-
-\tableofcontents
-
-\cleardoublepage\pagenumbering{arabic}
-
-\part{Elementary Techniques}
-\include{basics}
-\include{fp}
-\include{Documents/documents}
-
-\part{Logic and Sets}
-\include{Rules/rules}
-\include{Sets/sets}
-\include{Inductive/inductive}
-
-\part{Advanced Material}
-\include{Types/types}
-\include{Advanced/advanced}
-\include{Protocol/protocol}
-
-\markboth{}{}
-\cleardoublepage
-\vspace*{\fill}
-\begin{flushright}
-\begin{tabular}{l}
-{\large\sf\slshape You know my methods. Apply them!}\\[1ex]
-Sherlock Holmes
-\end{tabular}
-\end{flushright}
-\vspace*{\fill}
-\vspace*{\fill}
-
-\underscoreoff
-
-\include{appendix}
-
-\bibliographystyle{plain}
-\bibliography{../manual}
-\underscoreoff
-\printindex
-\end{document}