# HG changeset patch
# User paulson
# Date 994852484 -7200
# Node ID e143bb9d82553e3a964a8d165328f0ef574b0547
# Parent  26cbf43d76af30d0b9704835f2f9088f138ec6f6
separate preface and macro file

diff -r 26cbf43d76af -r e143bb9d8255 doc-src/TutorialI/tutorial.tex
--- 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}