# HG changeset patch
# User paulson
# Date 972315369 -7200
# Node ID b5fe1ab860fc6469e0bcf60439478b380b81ed43
# Parent  ab5617c3cefbc344d1136dbdb246b92068a5cac1
addition of Rules, Sets and some macros of lcp

diff -r ab5617c3cefb -r b5fe1ab860fc doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Mon Oct 23 17:35:39 2000 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Mon Oct 23 17:36:09 2000 +0200
@@ -1,7 +1,10 @@
 % pr(latex xsymbols symbols)
 \documentclass[11pt,a4paper]{report}
+\newif\ifremarks
+\remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
 \usepackage{isabelle,isabellesym}
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
+\usepackage{proof,amsmath}
 \usepackage{../pdfsetup}    %last package!
 
 %\newtheorem{theorem}{Theorem}[section]
@@ -22,6 +25,15 @@
 
 \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
+\let\bigisa=\isa
+%% was previously
+%% \newcommand{\bigisa}[1]{\texttt{\textsl{#1}}} 
+%% because \isa is too small for variables, but does it really matter?
+
+
 %%% 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}  
@@ -65,9 +77,8 @@
 
 \input{basics}
 \input{fp}
-\chapter{The Rules of the Game}
-\label{ch:Rules}
-\input{sets}
+\input{Rules/rules}
+\input{Sets/sets}\input{CTL/ctl}  %these constitute ONE chapter
 \input{Inductive/inductive}
 \input{Advanced/advanced}
 \chapter{More about Types}