diff -r 91886738773a -r 499435b4084e doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:55:35 2001 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:56:05 2001 +0200
@@ -67,7 +67,7 @@
 
 In Isabelle notation, the rule looks like this:
 \begin{isabelle}
-\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
+\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
 \end{isabelle}
 Carefully examine the syntax.  The premises appear to the
 left of the arrow and the conclusion to the right.  The premises (if 
@@ -159,7 +159,7 @@
 notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
 same  purpose:
 \begin{isabelle}
-\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
+\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
 \end{isabelle}
 When we use this sort of elimination rule backwards, it produces 
 a case split.  (We have seen this before, in proofs by induction.)  The following  proof
@@ -281,7 +281,7 @@
 alternative conjunction elimination rule that resembles \isa{disjE}\@.  It is
 seldom, if ever, seen in logic books.  In Isabelle syntax it looks like this: 
 \begin{isabelle}
-\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
+\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
 \end{isabelle}
 \index{destruction rules|)}
 
@@ -298,13 +298,13 @@
 in Isabelle: 
 \begin{isabelle}
 (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
-\isasymlongrightarrow\ ?Q\rulename{impI}
+\isasymlongrightarrow\ ?Q\rulenamedx{impI}
 \end{isabelle}
 And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}} :
 \begin{isabelle}
 \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
 \isasymLongrightarrow\ ?Q
-\rulename{mp}
+\rulenamedx{mp}
 \end{isabelle}
 
 Here is a proof using the implication rules.  This 
@@ -413,16 +413,16 @@
 presence of $\neg P$ together with~$P$: 
 \begin{isabelle}
 (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
-\rulename{notI}\isanewline
+\rulenamedx{notI}\isanewline
 \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
-\rulename{notE}
+\rulenamedx{notE}
 \end{isabelle}
 %
 Classical logic allows us to assume $\neg P$ 
 when attempting to prove~$P$: 
 \begin{isabelle}
 (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
-\rulename{classical}
+\rulenamedx{classical}
 \end{isabelle}
 
 \index{contrapositives|(}%
@@ -500,7 +500,7 @@
 peculiar but important rule, a form of disjunction introduction:
 \begin{isabelle}
 (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
-\rulename{disjCI}
+\rulenamedx{disjCI}
 \end{isabelle}
 This rule combines the effects of \isa{disjI1} and \isa{disjI2}.  Its great
 advantage is that we can remove the disjunction symbol without deciding
@@ -680,7 +680,7 @@
 \begin{isabelle}
 \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
 ?t
-\rulename{ssubst}
+\rulenamedx{ssubst}
 \end{isabelle}
 Crucially, \isa{?P} is a function 
 variable.  It can be replaced by a $\lambda$-term 
@@ -876,7 +876,7 @@
 Returning to the universal quantifier, we find that having a similar quantifier
 as part of the meta-logic makes the introduction rule trivial to express:
 \begin{isabelle}
-(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
+(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
 \end{isabelle}
 
 
@@ -910,7 +910,7 @@
 The conclusion is $P$ with $t$ substituted for the variable~$x$.  
 Isabelle expresses substitution using a function variable: 
 \begin{isabelle}
-{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
+{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
 \end{isabelle}
 This destruction rule takes a 
 universally quantified formula and removes the quantifier, replacing 
@@ -923,7 +923,7 @@
 appears in logic books:
 \begin{isabelle}
 \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
-\rulename{allE}
+\rulenamedx{allE}
 \end{isabelle}
 The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
 same inference.
@@ -1005,7 +1005,7 @@
 to the existential quantifier, whose introduction rule looks like this in
 Isabelle: 
 \begin{isabelle}
-?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
+?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
 \end{isabelle}
 If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
 P(x)$ is also true.  It is a dual of the universal elimination rule, and
@@ -1018,7 +1018,7 @@
 %
 It looks like this in Isabelle: 
 \begin{isabelle}
-\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
+\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
 \end{isabelle}
 %
 Given an existentially quantified theorem and some
@@ -1170,7 +1170,7 @@
 
 \medskip
 Existential formulas can be instantiated too.  The next example uses the 
-\textbf{divides} relation\indexbold{divides relation}
+\textbf{divides} relation\index{divides relation}
 of number theory: 
 \begin{isabelle}
 ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
@@ -1255,7 +1255,7 @@
 \begin{isabelle}
 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
 \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
-\rulename{some_equality}
+\rulenamedx{some_equality}
 \end{isabelle}
 For instance, we can define the
 cardinality of a finite set~$A$ to be that
@@ -1309,7 +1309,8 @@
 Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
 description}, when it makes an arbitrary selection from the values
 satisfying~\isa{P}\@.  Here is the definition
-of~\isa{inv},\index{*inv (constant)} which expresses inverses of functions:
+of~\cdx{inv}, which expresses inverses of
+functions:
 \begin{isabelle}
 inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
 \rulename{inv_def}
@@ -1335,10 +1336,10 @@
 tricky and requires rules such as these:
 \begin{isabelle}
 P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
-\rulename{someI}\isanewline
+\rulenamedx{someI}\isanewline
 \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
 x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
-\rulename{someI2}
+\rulenamedx{someI2}
 \end{isabelle}
 Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
 \hbox{\isa{SOME\ x.\ P\ x}}.  The repetition of~\isa{P} in the conclusion makes it
@@ -1838,7 +1839,7 @@
 ?s\ =\ ?t\
 \isasymLongrightarrow\ ?t\ =\
 ?s%
-\rulename{sym}
+\rulenamedx{sym}
 \end{isabelle}
 The following declaration gives our equation to \isa{sym}:
 \begin{isabelle}
@@ -1859,10 +1860,10 @@
 which extract  the two directions of reasoning about a boolean equivalence:
 \begin{isabelle}
 \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
-\rulename{iffD1}%
+\rulenamedx{iffD1}%
 \isanewline
 \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
-\rulename{iffD2}
+\rulenamedx{iffD2}
 \end{isabelle}
 %
 Normally we would never name the intermediate theorems
@@ -2017,7 +2018,7 @@
 such as these:
 \begin{isabelle}
 x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
-\rulename{arg_cong}\isanewline
+\rulenamedx{arg_cong}\isanewline
 i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
 \rulename{mult_le_mono1}
 \end{isabelle}
@@ -2096,8 +2097,8 @@
 is omitted.
 
 \medskip
-Here is another demonstration of \isa{insert}.  \REMARK{Effect with
-unknowns?} Division  and remainder obey a well-known law: 
+Here is another demonstration of \isa{insert}.  Division and
+remainder obey a well-known law: 
 \begin{isabelle}
 (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
 \rulename{mod_div_equality}