1.1 --- a/doc-src/TutorialI/tutorial.tex	Mon Oct 23 17:35:39 2000 +0200
     1.2 +++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 23 17:36:09 2000 +0200
     1.3 @@ -1,7 +1,10 @@
     1.4  % pr(latex xsymbols symbols)
     1.5  \documentclass[11pt,a4paper]{report}
     1.6 +\newif\ifremarks
     1.7 +\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
     1.8  \usepackage{isabelle,isabellesym}
     1.9  \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
    1.10 +\usepackage{proof,amsmath}
    1.11  \usepackage{../pdfsetup}    %last package!
    1.12  
    1.13  %\newtheorem{theorem}{Theorem}[section]
    1.14 @@ -22,6 +25,15 @@
    1.15  
    1.16  \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
    1.17  
    1.18 +%% lcp's macros
    1.19 +\newcommand{\remark}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
    1.20 +\newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
    1.21 +\let\bigisa=\isa
    1.22 +%% was previously
    1.23 +%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} 
    1.24 +%% because \isa is too small for variables, but does it really matter?
    1.25 +
    1.26 +
    1.27  %%% to index derived rls:  ^\([a-zA-Z0-9][a-zA-Z0-9_]*\)        \\tdx{\1}  
    1.28  %%% to index rulenames:   ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\),     \\tdx{\1}  
    1.29  %%% to index constants:   \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\)     \\cdx{\1}  
    1.30 @@ -65,9 +77,8 @@
    1.31  
    1.32  \input{basics}
    1.33  \input{fp}
    1.34 -\chapter{The Rules of the Game}
    1.35 -\label{ch:Rules}
    1.36 -\input{sets}
    1.37 +\input{Rules/rules}
    1.38 +\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
    1.39  \input{Inductive/inductive}
    1.40  \input{Advanced/advanced}
    1.41  \chapter{More about Types}