doc-src/TutorialI/tutorial.tex
changeset 11412 54dd65d0ae87
parent 11402 e143bb9d8255
child 11423 49312d90cf1f
     1.1 --- a/doc-src/TutorialI/tutorial.tex	Thu Jul 12 16:33:36 2001 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.tex	Thu Jul 12 16:36:26 2001 +0200
     1.3 @@ -1,46 +1,4 @@
     1.4 -\documentclass{article}
     1.5 -\usepackage{cl2emono-modified,isabelle,isabellesym}
     1.6 -\usepackage{../proof,amsmath,amsfonts}
     1.7 -\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
     1.8 -\usepackage{../pdfsetup}    %last package!
     1.9 -
    1.10 -\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
    1.11 -%\remarksfalse
    1.12 -
    1.13 -\makeindex
    1.14 -
    1.15 -\index{termination|see{total function}}
    1.16 -\index{product type|see{pair}}
    1.17 -\index{tuple|see{pair}}
    1.18 -\index{*<*lex*>|see{lexicographic product}}
    1.19 -
    1.20 -\underscoreoff
    1.21 -
    1.22 -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.23 -
    1.24 -\pagestyle{headings}
    1.25 -
    1.26 -
    1.27 -\begin{document}
    1.28 -\title{\includegraphics[scale=.8]{isabelle_hol}
    1.29 -       \\ \vspace{0.5cm} The Tutorial
    1.30 -       \\ --- DRAFT ---}
    1.31 -\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
    1.32 -Technische Universit{\"a}t M{\"u}nchen \\
    1.33 -Institut f{\"u}r Informatik \\[1ex]
    1.34 -University of Cambridge\\
    1.35 -Computer Laboratory}
    1.36 -\maketitle
    1.37 -
    1.38 -\pagenumbering{roman}
    1.39 -\setcounter{page}{5}
    1.40 -
    1.41 -\input{preface}
    1.42 -
    1.43 -\tableofcontents
    1.44 -
    1.45 -\newpage\pagenumbering{arabic}
    1.46 -
    1.47 +\documentclass{article}
    1.48 \usepackage{cl2emono-modified,isabelle,isabellesym}
    1.49 \usepackage{../proof,amsmath,amsfonts}
    1.50 \usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
    1.51 \usepackage{../pdfsetup}   
    1.52 %last package!
    1.53 
    1.54 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
    1.55 %\remarksfalse
    1.56 
    1.57 \makeindex
    1.58 
    1.59 \index{termination|see{total function}}
    1.60 \index{product type|see{pair}}
    1.61 \index{tuple|see{pair}}
    1.62 \index{*<*lex*>|see{lexicographic product}}
    1.63 
    1.64 \underscoreoff
    1.65 
    1.66 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.67 
    1.68 \pagestyle{headings}
    1.69 
    1.70 
    1.71 \begin{document}
    1.72 \title{\includegraphics[scale=.8]{isabelle_hol}
    1.73        \\ \vspace{0.5cm} The Tutorial
    1.74        \\ --- DRAFT ---}
    1.75 \author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
    1.76 Technische Universit{\"a}t M{\"u}nchen \\
    1.77 Institut f{\"u}r Informatik \\[1ex]
    1.78 University of Cambridge\\
    1.79 Computer Laboratory}
    1.80 \maketitle
    1.81 
    1.82 \pagenumbering{roman}
    1.83 \setcounter{page}{5}
    1.84 
    1.85 \input{preface}
    1.86 
    1.87 \tableofcontents
    1.88 
    1.89 \newpage\pagenumbering{arabic}
    1.90  \input{basics}
    1.91  \input{fp}
    1.92  \input{Rules/rules}