separate preface and macro file
authorpaulson
Wed Jul 11 13:54:44 2001 +0200 (2001-07-11)
changeset 11402e143bb9d8255
parent 11401 26cbf43d76af
child 11403 b3b95a228d37
separate preface and macro file
doc-src/TutorialI/tutorial.tex
     1.1 --- a/doc-src/TutorialI/tutorial.tex	Wed Jul 11 10:50:18 2001 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.tex	Wed Jul 11 13:54:44 2001 +0200
     1.3 @@ -1,46 +1,13 @@
     1.4  \documentclass{article}
     1.5 -\newif\ifremarks
     1.6 -\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
     1.7 -%\remarksfalse
     1.8  \usepackage{cl2emono-modified,isabelle,isabellesym}
     1.9  \usepackage{../proof,amsmath,amsfonts}
    1.10 -\usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
    1.11 +\usepackage{latexsym,verbatim,graphicx,tutorial,../ttbox,comment}
    1.12  \usepackage{../pdfsetup}    %last package!
    1.13  
    1.14 -%\newtheorem{theorem}{Theorem}[section]
    1.15 -\newtheorem{Exercise}{Exercise}[section]
    1.16 -\newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}}
    1.17 -\newcommand{\ttlbr}{\texttt{[|}}
    1.18 -\newcommand{\ttrbr}{\texttt{|]}}
    1.19 -\newcommand{\ttor}{\texttt{|}}
    1.20 -\newcommand{\ttall}{\texttt{!}}
    1.21 -\newcommand{\ttuniquex}{\texttt{?!}}
    1.22 -\newcommand{\ttEXU}{\texttt{EX!}}
    1.23 -\newcommand{\ttAnd}{\texttt{!!}}
    1.24 -
    1.25 -\newcommand{\isasymimp}{\isasymlongrightarrow}
    1.26 -\newcommand{\isasymImp}{\isasymLongrightarrow}
    1.27 -\newcommand{\isasymFun}{\isasymRightarrow}
    1.28 -\newcommand{\isasymuniqex}{\isamath{\exists!\,}}
    1.29 -\renewcommand{\S}{Sect.\ts}
    1.30 -
    1.31 -\renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
    1.32 -
    1.33 -%% lcp's macros
    1.34 -\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
    1.35 -\newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
    1.36 -
    1.37 -%%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.38 -%%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.39 -%%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.40 -%%% to deverbify:         \\verb|\([^|]*\)|     \\ttindex{\1}  
    1.41 -%% run    ../sedindex logics    to prepare index file
    1.42 +\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
    1.43 +%\remarksfalse
    1.44  
    1.45  \makeindex
    1.46 -\newcommand{\indexboldpos}[2]{#1\indexbold{#2@#1}}
    1.47 -\newcommand{\ttindexboldpos}[2]{\texttt{#1}\indexbold{#2@\texttt{#1}}}
    1.48 -\newcommand{\isaindexbold}[1]{\isa{#1}\index{*#1|bold}}
    1.49 -\newcommand{\isaindex}[1]{\isa{#1}\index{*#1}}
    1.50  
    1.51  \index{termination|see{total function}}
    1.52  \index{product type|see{pair}}
    1.53 @@ -52,8 +19,7 @@
    1.54  \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}  %% {secnumdepth}{2}???
    1.55  
    1.56  \pagestyle{headings}
    1.57 -%\sloppy
    1.58 -%\binperiod     %%%treat . like a binary operator
    1.59 +
    1.60  
    1.61  \begin{document}
    1.62  \title{\includegraphics[scale=.8]{isabelle_hol}
    1.63 @@ -67,15 +33,13 @@
    1.64  \maketitle
    1.65  
    1.66  \pagenumbering{roman}
    1.67 +\setcounter{page}{5}
    1.68 +
    1.69 +\input{preface}
    1.70 +
    1.71  \tableofcontents
    1.72  
    1.73 -\subsubsection*{Acknowledgements}
    1.74 -This tutorial owes a lot to the constant discussions with and the valuable
    1.75 -feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
    1.76 -Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch,
    1.77 -Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to
    1.78 -read and comment on a draft version.
    1.79 -\clearfirst
    1.80 +\newpage\pagenumbering{arabic}
    1.81  
    1.82  \input{basics}
    1.83  \input{fp}