--- a/doc-src/TutorialI/tutorial.tex Wed Jul 11 10:50:18 2001 +0200
+++ b/doc-src/TutorialI/tutorial.tex Wed Jul 11 13:54:44 2001 +0200
@@ -1,46 +1,13 @@
\documentclass{article}
-\newif\ifremarks
-\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
-%\remarksfalse
\usepackage{cl2emono-modified,isabelle,isabellesym}
\usepackage{../proof,amsmath,amsfonts}
-\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
+\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
\usepackage{../pdfsetup} %last package!
-%\newtheorem{theorem}{Theorem}[section]
-\newtheorem{Exercise}{Exercise}[section]
-\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
-\newcommand{\ttlbr}{\texttt{[|}}
-\newcommand{\ttrbr}{\texttt{|]}}
-\newcommand{\ttor}{\texttt{|}}
-\newcommand{\ttall}{\texttt{!}}
-\newcommand{\ttuniquex}{\texttt{?!}}
-\newcommand{\ttEXU}{\texttt{EX!}}
-\newcommand{\ttAnd}{\texttt{!!}}
-
-\newcommand{\isasymimp}{\isasymlongrightarrow}
-\newcommand{\isasymImp}{\isasymLongrightarrow}
-\newcommand{\isasymFun}{\isasymRightarrow}
-\newcommand{\isasymuniqex}{\isamath{\exists!\,}}
-\renewcommand{\S}{Sect.\ts}
-
-\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
-
-%% lcp's macros
-\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
-\newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
-
-%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
-%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
-%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
-%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
-%% run ../sedindex logics to prepare index file
+\remarkstrue %TRUE causes remarks to be displayed (as marginal notes)
+%\remarksfalse
\makeindex
-\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
-\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
-\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
-\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
\index{termination|see{total function}}
\index{product type|see{pair}}
@@ -52,8 +19,7 @@
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
\pagestyle{headings}
-%\sloppy
-%\binperiod %%%treat . like a binary operator
+
\begin{document}
\title{\includegraphics[scale=.8]{isabelle_hol}
@@ -67,15 +33,13 @@
\maketitle
\pagenumbering{roman}
+\setcounter{page}{5}
+
+\input{preface}
+
\tableofcontents
-\subsubsection*{Acknowledgements}
-This tutorial owes a lot to the constant discussions with and the valuable
-feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
-Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch,
-Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to
-read and comment on a draft version.
-\clearfirst
+\newpage\pagenumbering{arabic}
\input{basics}
\input{fp}