author paulson Wed, 11 Jul 2001 13:54:44 +0200 changeset 11402 e143bb9d8255 parent 11401 26cbf43d76af child 11403 b3b95a228d37
separate preface and macro file
--- 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}???

-%\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}