diff -r 1fead823c7c6 -r 6e15de7dd871 doc-src/TutorialI/tutorial.tex --- 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}