doc-src/TutorialI/tutorial.tex
 changeset 11423 49312d90cf1f parent 11412 54dd65d0ae87 child 11428 332347b9b942
     1.1 --- a/doc-src/TutorialI/tutorial.tex	Fri Jul 13 18:20:26 2001 +0200
1.2 +++ b/doc-src/TutorialI/tutorial.tex	Fri Jul 13 18:22:13 2001 +0200
1.3 @@ -1,4 +1,47 @@
1.4 -\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{termination|see{total function}}
\index{product type|see{pair}}
\index{tuple|see{pair}}
\index{*<*lex*>|see{lexicographic product}}

\underscoreoff

\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???

\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}
\setcounter{page}{5}

\input{preface}

\tableofcontents

\newpage\pagenumbering{arabic}
1.5 +\documentclass{article}
1.6 +\usepackage{cl2emono-modified,isabelle,isabellesym}
1.7 +\usepackage{../proof,amsmath,amsfonts}
1.8 +\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
1.9 +\usepackage{../pdfsetup}
1.10 +%last package!
1.11 +
1.12 +\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
1.13 +%\remarksfalse
1.14 +
1.15 +\makeindex
1.16 +
1.17 +\index{termination|see{total function}}
1.18 +\index{product type|see{pair}}
1.19 +\index{tuple|see{pair}}
1.20 +\index{*<*lex*>|see{lexicographic product}}
1.21 +
1.22 +\underscoreoff
1.23 +
1.24 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
1.25 +
1.27 +
1.28 +
1.29 +\begin{document}
1.30 +\title{\includegraphics[scale=.8]{isabelle_hol}
1.31 +       \\ \vspace{0.5cm} The Tutorial
1.32 +       \\ --- DRAFT ---}
1.33 +\author{Tobias Nipkow \& Lawrence Paulson\\[1ex]
1.34 +Technische Universit{\"a}t M{\"u}nchen \\
1.35 +Institut f{\"u}r Informatik \\[1ex]
1.36 +University of Cambridge\\
1.37 +Computer Laboratory}
1.38 +\maketitle
1.39 +
1.40 +\pagenumbering{roman}
1.41 +\setcounter{page}{5}
1.42 +
1.43 +\input{preface}
1.44 +
1.45 +\tableofcontents
1.46 +
1.47 +\newpage\pagenumbering{arabic}
1.48 +
1.49  \input{basics}
1.50  \input{fp}
1.51  \input{Rules/rules}