# HG changeset patch
# User paulson
# Date 995039765 -7200
# Node ID 499435b4084eaa27d9f59e84f0b0fe8b9c6e775f
# Parent  91886738773af30b8806456f08be1a0cad1f85b8
less indexing of theorem names

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}
diff -r 91886738773a -r 499435b4084e doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:55:35 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:56:05 2001 +0200
@@ -43,11 +43,11 @@
 \begin{isabelle}
 \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\ 
 \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%
-\rulename{IntI}\isanewline
+\rulenamedx{IntI}\isanewline
 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A
-\rulename{IntD1}\isanewline
+\rulenamedx{IntD1}\isanewline
 c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B
-\rulename{IntD2}
+\rulenamedx{IntD2}
 \end{isabelle}
 
 Here are two of the many installed theorems concerning set
@@ -55,7 +55,7 @@
 Note that it is denoted by a minus sign.
 \begin{isabelle}
 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
-\rulename{Compl_iff}\isanewline
+\rulenamedx{Compl_iff}\isanewline
 -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
 \rulename{Compl_Un}
 \end{isabelle}
@@ -75,12 +75,12 @@
 are its natural deduction rules:
 \begin{isabelle}
 ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%
-\rulename{subsetI}%
+\rulenamedx{subsetI}%
 \par\smallskip%          \isanewline didn't leave enough space
 \isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\
 A\isasymrbrakk\ \isasymLongrightarrow\ c\
 \isasymin\ B%
-\rulename{subsetD}
+\rulenamedx{subsetD}
 \end{isabelle}
 In harder proofs, you may need to apply \isa{subsetD} giving a specific term
 for~\isa{c}.  However, \isa{blast} can instantly prove facts such as this
@@ -88,7 +88,7 @@
 \begin{isabelle}
 (A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\
 (A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)
-\rulename{Un_subset_iff}
+\rulenamedx{Un_subset_iff}
 \end{isabelle}
 Here is another example, also proved automatically:
 \begin{isabelle}
@@ -125,7 +125,7 @@
 \begin{isabelle}
 ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\
 {\isasymLongrightarrow}\ A\ =\ B
-\rulename{set_ext}
+\rulenamedx{set_ext}
 \end{isabelle}
 Extensionality can be expressed as 
 $A=B\iff (A\subseteq B)\conj (B\subseteq A)$.  
@@ -135,12 +135,12 @@
 \begin{isabelle}
 \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\
 A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B
-\rulename{equalityI}
+\rulenamedx{equalityI}
 \par\smallskip%          \isanewline didn't leave enough space
 \isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\
 \isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\
 \isasymLongrightarrow\ P%
-\rulename{equalityE}
+\rulenamedx{equalityE}
 \end{isabelle}
 
 
@@ -264,13 +264,13 @@
 \begin{isabelle}
 ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin
 A.\ P\ x%
-\rulename{ballI}%
+\rulenamedx{ballI}%
 \isanewline
 \isasymlbrakk{\isasymforall}x\isasymin A.\
 P\ x;\ x\ \isasymin\
 A\isasymrbrakk\ \isasymLongrightarrow\ P\
 x%
-\rulename{bspec}
+\rulenamedx{bspec}
 \end{isabelle}
 %
 Dually, here are the natural deduction rules for the
@@ -282,14 +282,14 @@
 \isasymLongrightarrow\
 \isasymexists x\isasymin A.\ P\
 x%
-\rulename{bexI}%
+\rulenamedx{bexI}%
 \isanewline
 \isasymlbrakk\isasymexists x\isasymin A.\
 P\ x;\ {\isasymAnd}x.\
 {\isasymlbrakk}x\ \isasymin\ A;\
 P\ x\isasymrbrakk\ \isasymLongrightarrow\
 Q\isasymrbrakk\ \isasymLongrightarrow\ Q%
-\rulename{bexE}
+\rulenamedx{bexE}
 \end{isabelle}
 \index{quantifiers!for sets|)}
 
@@ -301,7 +301,7 @@
 (b\ \isasymin\
 (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
-\rulename{UN_iff}
+\rulenamedx{UN_iff}
 \end{isabelle}
 It has two natural deduction rules similar to those for the existential
 quantifier.  Sometimes \isa{UN_I} must be applied explicitly:
@@ -312,7 +312,7 @@
 b\ \isasymin\
 ({\isasymUnion}x\isasymin A.\
 B\ x)
-\rulename{UN_I}%
+\rulenamedx{UN_I}%
 \isanewline
 \isasymlbrakk b\ \isasymin\
 ({\isasymUnion}x\isasymin A.\
@@ -321,7 +321,7 @@
 A;\ b\ \isasymin\
 B\ x\isasymrbrakk\ \isasymLongrightarrow\
 R\isasymrbrakk\ \isasymLongrightarrow\ R%
-\rulename{UN_E}
+\rulenamedx{UN_E}
 \end{isabelle}
 %
 The following built-in syntax translation (see \S\ref{sec:def-translations})
@@ -341,7 +341,7 @@
 \begin{isabelle}
 (A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\
 \isasymin\ X)
-\rulename{Union_iff}
+\rulenamedx{Union_iff}
 \end{isabelle}
 
 \index{intersection!indexed}%
@@ -356,13 +356,13 @@
 =\
 ({\isasymforall}x\isasymin A.\
 b\ \isasymin\ B\ x)
-\rulename{INT_iff}%
+\rulenamedx{INT_iff}%
 \isanewline
 (A\ \isasymin\
 \isasymInter C)\ =\
 ({\isasymforall}X\isasymin C.\
 A\ \isasymin\ X)
-\rulename{Inter_iff}
+\rulenamedx{Inter_iff}
 \end{isabelle}
 
 Isabelle uses logical equivalences such as those above in automatic proof. 
@@ -404,12 +404,12 @@
 \begin{isabelle}
 {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline
 \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)
-\rulename{card_Un_Int}%
+\rulenamedx{card_Un_Int}%
 \isanewline
 \isanewline
 finite\ A\ \isasymLongrightarrow\ card\
 (Pow\ A)\  =\ 2\ \isacharcircum\ card\ A%
-\rulename{card_Pow}%
+\rulenamedx{card_Pow}%
 \isanewline
 \isanewline
 finite\ A\ \isasymLongrightarrow\isanewline
@@ -449,7 +449,7 @@
 functions:
 \begin{isabelle}
 ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g
-\rulename{ext}
+\rulenamedx{ext}
 \end{isabelle}
 
 \indexbold{updating a function}%
@@ -478,11 +478,11 @@
 defined:
 \begin{isabelle}%
 id\ \isasymequiv\ {\isasymlambda}x.\ x%
-\rulename{id_def}\isanewline
+\rulenamedx{id_def}\isanewline
 f\ \isasymcirc\ g\ \isasymequiv\
 {\isasymlambda}x.\ f\
 (g\ x)%
-\rulename{o_def}
+\rulenamedx{o_def}
 \end{isabelle}
 %
 Many familiar theorems concerning the identity and composition 
@@ -500,12 +500,12 @@
 inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\
 {\isasymforall}y\isasymin  A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\
 =\ y%
-\rulename{inj_on_def}\isanewline
+\rulenamedx{inj_on_def}\isanewline
 surj\ f\ \isasymequiv\ {\isasymforall}y.\
 \isasymexists x.\ y\ =\ f\ x%
-\rulename{surj_def}\isanewline
+\rulenamedx{surj_def}\isanewline
 bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f
-\rulename{bij_def}
+\rulenamedx{bij_def}
 \end{isabelle}
 The second argument
 of \isa{inj_on} lets us express that a function is injective over a
@@ -588,7 +588,7 @@
 \begin{isabelle}
 f\ `\ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin
 A.\ y\ =\ f\ x\isacharbraceright
-\rulename{image_def}
+\rulenamedx{image_def}
 \end{isabelle}
 %
 Here are some of the many facts proved about image: 
@@ -637,7 +637,7 @@
 It is defined as follows: 
 \begin{isabelle}
 f\ -`\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright
-\rulename{vimage_def}
+\rulenamedx{vimage_def}
 \end{isabelle}
 %
 This is one of the facts proved about it:
@@ -662,7 +662,7 @@
 definition: 
 \begin{isabelle}
 Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}%
-\rulename{Id_def}
+\rulenamedx{Id_def}
 \end{isabelle}
 
 \indexbold{composition!of relations}%
@@ -670,7 +670,7 @@
 available: 
 \begin{isabelle}
 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
-\rulename{comp_def}
+\rulenamedx{comp_def}
 \end{isabelle}
 %
 This is one of the many lemmas proved about these concepts: 
@@ -698,7 +698,7 @@
 \begin{isabelle}
 ((a,b)\ \isasymin\ r\isasyminverse)\ =\
 ((b,a)\ \isasymin\ r)
-\rulename{converse_iff}
+\rulenamedx{converse_iff}
 \end{isabelle}
 %
 Here is a typical law proved about converse and composition: 
@@ -713,7 +713,7 @@
 \begin{isabelle}
 (b\ \isasymin\ r\ ``\ A)\ =\ (\isasymexists x\isasymin
 A.\ (x,b)\ \isasymin\ r)
-\rulename{Image_iff}
+\rulenamedx{Image_iff}
 \end{isabelle}
 It satisfies many similar laws.
 
@@ -724,13 +724,13 @@
 \begin{isabelle}
 (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\
 r)
-\rulename{Domain_iff}%
+\rulenamedx{Domain_iff}%
 \isanewline
 (a\ \isasymin\ Range\ r)\
 \ =\ (\isasymexists y.\
 (y,a)\
 \isasymin\ r)
-\rulename{Range_iff}
+\rulenamedx{Range_iff}
 \end{isabelle}
 
 Iterated composition of a relation is available.  The notation overloads 
@@ -757,13 +757,13 @@
 rules:
 \begin{isabelle}
 (a,\ a)\ \isasymin \ r\isactrlsup *
-\rulename{rtrancl_refl}\isanewline
+\rulenamedx{rtrancl_refl}\isanewline
 p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
-\rulename{r_into_rtrancl}\isanewline
+\rulenamedx{r_into_rtrancl}\isanewline
 \isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\ 
 (b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
 (a,c)\ \isasymin \ r\isactrlsup *
-\rulename{rtrancl_trans}
+\rulenamedx{rtrancl_trans}
 \end{isabelle}
 %
 Induction over the reflexive transitive closure is available: 
@@ -785,9 +785,9 @@
 \isa{r\isacharcircum+}.  It has two  introduction rules: 
 \begin{isabelle}
 p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
-\rulename{r_into_trancl}\isanewline
+\rulenamedx{r_into_trancl}\isanewline
 \isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
-\rulename{trancl_trans}
+\rulenamedx{trancl_trans}
 \end{isabelle}
 %
 The induction rule resembles the one shown above. 
@@ -910,7 +910,7 @@
 relation  behaves as expected and that it is well-founded: 
 \begin{isabelle}
 ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
-\rulename{less_than_iff}\isanewline
+\rulenamedx{less_than_iff}\isanewline
 wf\ less_than
 \rulename{wf_less_than}
 \end{isabelle}
@@ -925,7 +925,7 @@
 \begin{isabelle}
 inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\
 \isasymin\ r\isacharbraceright
-\rulename{inv_image_def}\isanewline
+\rulenamedx{inv_image_def}\isanewline
 wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
 \rulename{wf_inv_image}
 \end{isabelle}
@@ -936,7 +936,7 @@
 \isa{measure} as shown: 
 \begin{isabelle}
 measure\ \isasymequiv\ inv_image\ less_than%
-\rulename{measure_def}\isanewline
+\rulenamedx{measure_def}\isanewline
 wf\ (measure\ f)
 \rulename{wf_measure}
 \end{isabelle}
@@ -953,7 +953,7 @@
 \isasymor\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\
 \isasymin \ rb\isacharbraceright 
-\rulename{lex_prod_def}%
+\rulenamedx{lex_prod_def}%
 \par\smallskip
 \isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
 \rulename{wf_lex_prod}
@@ -986,7 +986,7 @@
   {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
 \isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
 \isasymLongrightarrow\ P\ a
-\rulename{wf_induct}
+\rulenamedx{wf_induct}
 \end{isabelle}
 Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
 
@@ -1021,7 +1021,7 @@
 Isabelle's definition of monotone is overloaded over all orderings:
 \begin{isabelle}
 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
-\rulename{mono_def}
+\rulenamedx{mono_def}
 \end{isabelle}
 %
 For fixed point operators, the ordering will be the subset relation: if