# HG changeset patch
# User paulson
# Date 973531702 -3600
# Node ID e37e123738f75c66f685c2a446ec126445d59d23
# Parent  cdb451206ef9d99a7fe881b9f1bd693fe3e0a805
minor modifications for new Springer style

diff -r cdb451206ef9 -r e37e123738f7 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Mon Nov 06 16:43:01 2000 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Mon Nov 06 18:28:22 2000 +0100
@@ -1,4 +1,3 @@
-% ID:         $Id$
 \chapter{The Rules of the Game}
 \label{chap:rules}
  
@@ -898,7 +897,7 @@
 the universal introduction  rule, the textbook version imposes a proviso on the
 quantified variable, which Isabelle expresses using its meta-logic.  Note that it is
 enough to have a universal quantifier in the meta-logic; we do not need an existential
-quantifier to be built in as well.\remark{EX example needed?}
+quantifier to be built in as well.\REMARK{EX example needed?}
  
 Isabelle/HOL also provides Hilbert's
 $\epsilon$-operator.  The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is
@@ -910,7 +909,7 @@
 uniquely.  For instance, we can define the cardinality of a finite set~$A$ to be that
 $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$.  We can then
 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
-description) and proceed to prove other facts.\remark{SOME theorems
+description) and proceed to prove other facts.\REMARK{SOME theorems
 and example}
 
 \begin{exercise}
@@ -1160,7 +1159,7 @@
 \end{isabelle}
 %
 This fact about multiplication is also appropriate for 
-the {\isa{iff}} attribute:\remark{the ?s are ugly here but we need
+the {\isa{iff}} attribute:\REMARK{the ?s are ugly here but we need
 them again when talking about \isa{of}; we need a consistent style}
 \begin{isabelle}
 (\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
@@ -1412,7 +1411,7 @@
 
 The {\isa{force}} method applies the classical reasoner and simplifier 
 to one goal. 
-\remark{example needed? most
+\REMARK{example needed? most
 things done by blast, simp or auto can also be done by force, so why add a new
 one?}
 Unless it can prove the goal, it fails. Contrast 
@@ -1574,7 +1573,7 @@
 ?n)\ =\ k%
 \end{isabelle}
 \isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the
-resulting conclusion.\remark{figure necessary?}  The effect is to exchange the
+resulting conclusion.\REMARK{figure necessary?}  The effect is to exchange the
 two operands of the equality. Typically {\isa{THEN}} is used with destruction
 rules.  Above we have used
 \isa{THEN~conjunct1} to extract the first part of the theorem
@@ -1765,7 +1764,7 @@
 complete the proof. 
 
 \medskip
-Here is another proof using \isa{insert}.  \remark{Effect with unknowns?}
+Here is another proof using \isa{insert}.  \REMARK{Effect with unknowns?}
 Division  and remainder obey a well-known law: 
 \begin{isabelle}
 (?m\ div\ ?n)\ \isacharasterisk\
diff -r cdb451206ef9 -r e37e123738f7 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 16:43:01 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 18:28:22 2000 +0100
@@ -841,7 +841,7 @@
 \end{isabelle}
 
 Note one detail. The {\isa{auto}} method can prove this but
-{\isa{blast}} cannot. \remark{move to a later section?}
+{\isa{blast}} cannot. \REMARK{move to a later section?}
 This is because the
 lemmas we have proved only apply  to ordered pairs. {\isa{Auto}} can
 convert a bound variable of  a product type into a pair of bound variables,
diff -r cdb451206ef9 -r e37e123738f7 doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Mon Nov 06 16:43:01 2000 +0100
+++ b/doc-src/TutorialI/tutorial.tex	Mon Nov 06 18:28:22 2000 +0100
@@ -1,8 +1,8 @@
 % pr(latex xsymbols symbols)
-\documentclass[11pt,a4paper]{report}
+\documentclass{article}
 \newif\ifremarks
 \remarkstrue          %TRUE causes remarks to be displayed (as marginal notes)
-\usepackage{isabelle,isabellesym}
+\usepackage{cl2emono-modified,isabelle,isabellesym}
 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment}
 \usepackage{proof,amsmath}
 \usepackage{../pdfsetup}    %last package!
@@ -26,7 +26,7 @@
 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}}
 
 %% lcp's macros
-\newcommand{\remark}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
+\newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi}
 \newcommand{\rulename}[1]{\hfill$(\text{#1})$} %names of Isabelle rules
 \let\bigisa=\isa
 %% was previously