less indexing of theorem names
authorpaulson
Fri Jul 13 17:56:05 2001 +0200 (2001-07-13)
changeset 11417499435b4084e
parent 11416 91886738773a
child 11418 53a402c10ba9
less indexing of theorem names
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
     1.1 --- a/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:55:35 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jul 13 17:56:05 2001 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  
     1.5  In Isabelle notation, the rule looks like this:
     1.6  \begin{isabelle}
     1.7 -\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI}
     1.8 +\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI}
     1.9  \end{isabelle}
    1.10  Carefully examine the syntax.  The premises appear to the
    1.11  left of the arrow and the conclusion to the right.  The premises (if 
    1.12 @@ -159,7 +159,7 @@
    1.13  notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the
    1.14  same  purpose:
    1.15  \begin{isabelle}
    1.16 -\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE}
    1.17 +\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE}
    1.18  \end{isabelle}
    1.19  When we use this sort of elimination rule backwards, it produces 
    1.20  a case split.  (We have seen this before, in proofs by induction.)  The following  proof
    1.21 @@ -281,7 +281,7 @@
    1.22  alternative conjunction elimination rule that resembles \isa{disjE}\@.  It is
    1.23  seldom, if ever, seen in logic books.  In Isabelle syntax it looks like this: 
    1.24  \begin{isabelle}
    1.25 -\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE}
    1.26 +\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE}
    1.27  \end{isabelle}
    1.28  \index{destruction rules|)}
    1.29  
    1.30 @@ -298,13 +298,13 @@
    1.31  in Isabelle: 
    1.32  \begin{isabelle}
    1.33  (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\
    1.34 -\isasymlongrightarrow\ ?Q\rulename{impI}
    1.35 +\isasymlongrightarrow\ ?Q\rulenamedx{impI}
    1.36  \end{isabelle}
    1.37  And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}} :
    1.38  \begin{isabelle}
    1.39  \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\
    1.40  \isasymLongrightarrow\ ?Q
    1.41 -\rulename{mp}
    1.42 +\rulenamedx{mp}
    1.43  \end{isabelle}
    1.44  
    1.45  Here is a proof using the implication rules.  This 
    1.46 @@ -413,16 +413,16 @@
    1.47  presence of $\neg P$ together with~$P$: 
    1.48  \begin{isabelle}
    1.49  (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P%
    1.50 -\rulename{notI}\isanewline
    1.51 +\rulenamedx{notI}\isanewline
    1.52  \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R%
    1.53 -\rulename{notE}
    1.54 +\rulenamedx{notE}
    1.55  \end{isabelle}
    1.56  %
    1.57  Classical logic allows us to assume $\neg P$ 
    1.58  when attempting to prove~$P$: 
    1.59  \begin{isabelle}
    1.60  (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P%
    1.61 -\rulename{classical}
    1.62 +\rulenamedx{classical}
    1.63  \end{isabelle}
    1.64  
    1.65  \index{contrapositives|(}%
    1.66 @@ -500,7 +500,7 @@
    1.67  peculiar but important rule, a form of disjunction introduction:
    1.68  \begin{isabelle}
    1.69  (\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q%
    1.70 -\rulename{disjCI}
    1.71 +\rulenamedx{disjCI}
    1.72  \end{isabelle}
    1.73  This rule combines the effects of \isa{disjI1} and \isa{disjI2}.  Its great
    1.74  advantage is that we can remove the disjunction symbol without deciding
    1.75 @@ -680,7 +680,7 @@
    1.76  \begin{isabelle}
    1.77  \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\
    1.78  ?t
    1.79 -\rulename{ssubst}
    1.80 +\rulenamedx{ssubst}
    1.81  \end{isabelle}
    1.82  Crucially, \isa{?P} is a function 
    1.83  variable.  It can be replaced by a $\lambda$-term 
    1.84 @@ -876,7 +876,7 @@
    1.85  Returning to the universal quantifier, we find that having a similar quantifier
    1.86  as part of the meta-logic makes the introduction rule trivial to express:
    1.87  \begin{isabelle}
    1.88 -(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
    1.89 +(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI}
    1.90  \end{isabelle}
    1.91  
    1.92  
    1.93 @@ -910,7 +910,7 @@
    1.94  The conclusion is $P$ with $t$ substituted for the variable~$x$.  
    1.95  Isabelle expresses substitution using a function variable: 
    1.96  \begin{isabelle}
    1.97 -{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec}
    1.98 +{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec}
    1.99  \end{isabelle}
   1.100  This destruction rule takes a 
   1.101  universally quantified formula and removes the quantifier, replacing 
   1.102 @@ -923,7 +923,7 @@
   1.103  appears in logic books:
   1.104  \begin{isabelle}
   1.105  \isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R%
   1.106 -\rulename{allE}
   1.107 +\rulenamedx{allE}
   1.108  \end{isabelle}
   1.109  The methods \isa{drule~spec} and \isa{erule~allE} do precisely the
   1.110  same inference.
   1.111 @@ -1005,7 +1005,7 @@
   1.112  to the existential quantifier, whose introduction rule looks like this in
   1.113  Isabelle: 
   1.114  \begin{isabelle}
   1.115 -?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI}
   1.116 +?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI}
   1.117  \end{isabelle}
   1.118  If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x.
   1.119  P(x)$ is also true.  It is a dual of the universal elimination rule, and
   1.120 @@ -1018,7 +1018,7 @@
   1.121  %
   1.122  It looks like this in Isabelle: 
   1.123  \begin{isabelle}
   1.124 -\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
   1.125 +\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE}
   1.126  \end{isabelle}
   1.127  %
   1.128  Given an existentially quantified theorem and some
   1.129 @@ -1170,7 +1170,7 @@
   1.130  
   1.131  \medskip
   1.132  Existential formulas can be instantiated too.  The next example uses the 
   1.133 -\textbf{divides} relation\indexbold{divides relation}
   1.134 +\textbf{divides} relation\index{divides relation}
   1.135  of number theory: 
   1.136  \begin{isabelle}
   1.137  ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
   1.138 @@ -1255,7 +1255,7 @@
   1.139  \begin{isabelle}
   1.140  \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 
   1.141  \isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a%
   1.142 -\rulename{some_equality}
   1.143 +\rulenamedx{some_equality}
   1.144  \end{isabelle}
   1.145  For instance, we can define the
   1.146  cardinality of a finite set~$A$ to be that
   1.147 @@ -1309,7 +1309,8 @@
   1.148  Occasionally, \hbox{\isa{SOME\ x.\ P\ x}} serves as an \textbf{indefinite
   1.149  description}, when it makes an arbitrary selection from the values
   1.150  satisfying~\isa{P}\@.  Here is the definition
   1.151 -of~\isa{inv},\index{*inv (constant)} which expresses inverses of functions:
   1.152 +of~\cdx{inv}, which expresses inverses of
   1.153 +functions:
   1.154  \begin{isabelle}
   1.155  inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y%
   1.156  \rulename{inv_def}
   1.157 @@ -1335,10 +1336,10 @@
   1.158  tricky and requires rules such as these:
   1.159  \begin{isabelle}
   1.160  P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x)
   1.161 -\rulename{someI}\isanewline
   1.162 +\rulenamedx{someI}\isanewline
   1.163  \isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\
   1.164  x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x)
   1.165 -\rulename{someI2}
   1.166 +\rulenamedx{someI2}
   1.167  \end{isabelle}
   1.168  Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does
   1.169  \hbox{\isa{SOME\ x.\ P\ x}}.  The repetition of~\isa{P} in the conclusion makes it
   1.170 @@ -1838,7 +1839,7 @@
   1.171  ?s\ =\ ?t\
   1.172  \isasymLongrightarrow\ ?t\ =\
   1.173  ?s%
   1.174 -\rulename{sym}
   1.175 +\rulenamedx{sym}
   1.176  \end{isabelle}
   1.177  The following declaration gives our equation to \isa{sym}:
   1.178  \begin{isabelle}
   1.179 @@ -1859,10 +1860,10 @@
   1.180  which extract  the two directions of reasoning about a boolean equivalence:
   1.181  \begin{isabelle}
   1.182  \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
   1.183 -\rulename{iffD1}%
   1.184 +\rulenamedx{iffD1}%
   1.185  \isanewline
   1.186  \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
   1.187 -\rulename{iffD2}
   1.188 +\rulenamedx{iffD2}
   1.189  \end{isabelle}
   1.190  %
   1.191  Normally we would never name the intermediate theorems
   1.192 @@ -2017,7 +2018,7 @@
   1.193  such as these:
   1.194  \begin{isabelle}
   1.195  x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y%
   1.196 -\rulename{arg_cong}\isanewline
   1.197 +\rulenamedx{arg_cong}\isanewline
   1.198  i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k%
   1.199  \rulename{mult_le_mono1}
   1.200  \end{isabelle}
   1.201 @@ -2096,8 +2097,8 @@
   1.202  is omitted.
   1.203  
   1.204  \medskip
   1.205 -Here is another demonstration of \isa{insert}.  \REMARK{Effect with
   1.206 -unknowns?} Division  and remainder obey a well-known law: 
   1.207 +Here is another demonstration of \isa{insert}.  Division and
   1.208 +remainder obey a well-known law: 
   1.209  \begin{isabelle}
   1.210  (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
   1.211  \rulename{mod_div_equality}
     2.1 --- a/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:55:35 2001 +0200
     2.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jul 13 17:56:05 2001 +0200
     2.3 @@ -43,11 +43,11 @@
     2.4  \begin{isabelle}
     2.5  \isasymlbrakk c\ \isasymin\ A;\ c\ \isasymin\ B\isasymrbrakk\ 
     2.6  \isasymLongrightarrow\ c\ \isasymin\ A\ \isasyminter\ B%
     2.7 -\rulename{IntI}\isanewline
     2.8 +\rulenamedx{IntI}\isanewline
     2.9  c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ A
    2.10 -\rulename{IntD1}\isanewline
    2.11 +\rulenamedx{IntD1}\isanewline
    2.12  c\ \isasymin\ A\ \isasyminter\ B\ \isasymLongrightarrow\ c\ \isasymin\ B
    2.13 -\rulename{IntD2}
    2.14 +\rulenamedx{IntD2}
    2.15  \end{isabelle}
    2.16  
    2.17  Here are two of the many installed theorems concerning set
    2.18 @@ -55,7 +55,7 @@
    2.19  Note that it is denoted by a minus sign.
    2.20  \begin{isabelle}
    2.21  (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
    2.22 -\rulename{Compl_iff}\isanewline
    2.23 +\rulenamedx{Compl_iff}\isanewline
    2.24  -\ (A\ \isasymunion\ B)\ =\ -\ A\ \isasyminter\ -\ B
    2.25  \rulename{Compl_Un}
    2.26  \end{isabelle}
    2.27 @@ -75,12 +75,12 @@
    2.28  are its natural deduction rules:
    2.29  \begin{isabelle}
    2.30  ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ x\ \isasymin\ B)\ \isasymLongrightarrow\ A\ \isasymsubseteq\ B%
    2.31 -\rulename{subsetI}%
    2.32 +\rulenamedx{subsetI}%
    2.33  \par\smallskip%          \isanewline didn't leave enough space
    2.34  \isasymlbrakk A\ \isasymsubseteq\ B;\ c\ \isasymin\
    2.35  A\isasymrbrakk\ \isasymLongrightarrow\ c\
    2.36  \isasymin\ B%
    2.37 -\rulename{subsetD}
    2.38 +\rulenamedx{subsetD}
    2.39  \end{isabelle}
    2.40  In harder proofs, you may need to apply \isa{subsetD} giving a specific term
    2.41  for~\isa{c}.  However, \isa{blast} can instantly prove facts such as this
    2.42 @@ -88,7 +88,7 @@
    2.43  \begin{isabelle}
    2.44  (A\ \isasymunion\ B\ \isasymsubseteq\ C)\ =\
    2.45  (A\ \isasymsubseteq\ C\ \isasymand\ B\ \isasymsubseteq\ C)
    2.46 -\rulename{Un_subset_iff}
    2.47 +\rulenamedx{Un_subset_iff}
    2.48  \end{isabelle}
    2.49  Here is another example, also proved automatically:
    2.50  \begin{isabelle}
    2.51 @@ -125,7 +125,7 @@
    2.52  \begin{isabelle}
    2.53  ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\
    2.54  {\isasymLongrightarrow}\ A\ =\ B
    2.55 -\rulename{set_ext}
    2.56 +\rulenamedx{set_ext}
    2.57  \end{isabelle}
    2.58  Extensionality can be expressed as 
    2.59  $A=B\iff (A\subseteq B)\conj (B\subseteq A)$.  
    2.60 @@ -135,12 +135,12 @@
    2.61  \begin{isabelle}
    2.62  \isasymlbrakk A\ \isasymsubseteq\ B;\ B\ \isasymsubseteq\
    2.63  A\isasymrbrakk\ \isasymLongrightarrow\ A\ =\ B
    2.64 -\rulename{equalityI}
    2.65 +\rulenamedx{equalityI}
    2.66  \par\smallskip%          \isanewline didn't leave enough space
    2.67  \isasymlbrakk A\ =\ B;\ \isasymlbrakk A\ \isasymsubseteq\ B;\ B\
    2.68  \isasymsubseteq\ A\isasymrbrakk\ \isasymLongrightarrow\ P\isasymrbrakk\
    2.69  \isasymLongrightarrow\ P%
    2.70 -\rulename{equalityE}
    2.71 +\rulenamedx{equalityE}
    2.72  \end{isabelle}
    2.73  
    2.74  
    2.75 @@ -264,13 +264,13 @@
    2.76  \begin{isabelle}
    2.77  ({\isasymAnd}x.\ x\ \isasymin\ A\ \isasymLongrightarrow\ P\ x)\ \isasymLongrightarrow\ {\isasymforall}x\isasymin
    2.78  A.\ P\ x%
    2.79 -\rulename{ballI}%
    2.80 +\rulenamedx{ballI}%
    2.81  \isanewline
    2.82  \isasymlbrakk{\isasymforall}x\isasymin A.\
    2.83  P\ x;\ x\ \isasymin\
    2.84  A\isasymrbrakk\ \isasymLongrightarrow\ P\
    2.85  x%
    2.86 -\rulename{bspec}
    2.87 +\rulenamedx{bspec}
    2.88  \end{isabelle}
    2.89  %
    2.90  Dually, here are the natural deduction rules for the
    2.91 @@ -282,14 +282,14 @@
    2.92  \isasymLongrightarrow\
    2.93  \isasymexists x\isasymin A.\ P\
    2.94  x%
    2.95 -\rulename{bexI}%
    2.96 +\rulenamedx{bexI}%
    2.97  \isanewline
    2.98  \isasymlbrakk\isasymexists x\isasymin A.\
    2.99  P\ x;\ {\isasymAnd}x.\
   2.100  {\isasymlbrakk}x\ \isasymin\ A;\
   2.101  P\ x\isasymrbrakk\ \isasymLongrightarrow\
   2.102  Q\isasymrbrakk\ \isasymLongrightarrow\ Q%
   2.103 -\rulename{bexE}
   2.104 +\rulenamedx{bexE}
   2.105  \end{isabelle}
   2.106  \index{quantifiers!for sets|)}
   2.107  
   2.108 @@ -301,7 +301,7 @@
   2.109  (b\ \isasymin\
   2.110  (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
   2.111  b\ \isasymin\ B\ x)
   2.112 -\rulename{UN_iff}
   2.113 +\rulenamedx{UN_iff}
   2.114  \end{isabelle}
   2.115  It has two natural deduction rules similar to those for the existential
   2.116  quantifier.  Sometimes \isa{UN_I} must be applied explicitly:
   2.117 @@ -312,7 +312,7 @@
   2.118  b\ \isasymin\
   2.119  ({\isasymUnion}x\isasymin A.\
   2.120  B\ x)
   2.121 -\rulename{UN_I}%
   2.122 +\rulenamedx{UN_I}%
   2.123  \isanewline
   2.124  \isasymlbrakk b\ \isasymin\
   2.125  ({\isasymUnion}x\isasymin A.\
   2.126 @@ -321,7 +321,7 @@
   2.127  A;\ b\ \isasymin\
   2.128  B\ x\isasymrbrakk\ \isasymLongrightarrow\
   2.129  R\isasymrbrakk\ \isasymLongrightarrow\ R%
   2.130 -\rulename{UN_E}
   2.131 +\rulenamedx{UN_E}
   2.132  \end{isabelle}
   2.133  %
   2.134  The following built-in syntax translation (see \S\ref{sec:def-translations})
   2.135 @@ -341,7 +341,7 @@
   2.136  \begin{isabelle}
   2.137  (A\ \isasymin\ \isasymUnion C)\ =\ (\isasymexists X\isasymin C.\ A\
   2.138  \isasymin\ X)
   2.139 -\rulename{Union_iff}
   2.140 +\rulenamedx{Union_iff}
   2.141  \end{isabelle}
   2.142  
   2.143  \index{intersection!indexed}%
   2.144 @@ -356,13 +356,13 @@
   2.145  =\
   2.146  ({\isasymforall}x\isasymin A.\
   2.147  b\ \isasymin\ B\ x)
   2.148 -\rulename{INT_iff}%
   2.149 +\rulenamedx{INT_iff}%
   2.150  \isanewline
   2.151  (A\ \isasymin\
   2.152  \isasymInter C)\ =\
   2.153  ({\isasymforall}X\isasymin C.\
   2.154  A\ \isasymin\ X)
   2.155 -\rulename{Inter_iff}
   2.156 +\rulenamedx{Inter_iff}
   2.157  \end{isabelle}
   2.158  
   2.159  Isabelle uses logical equivalences such as those above in automatic proof. 
   2.160 @@ -404,12 +404,12 @@
   2.161  \begin{isabelle}
   2.162  {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline
   2.163  \isasymLongrightarrow\ card\ A\ \isacharplus\ card\ B\ =\ card\ (A\ \isasymunion\ B)\ \isacharplus\ card\ (A\ \isasyminter\ B)
   2.164 -\rulename{card_Un_Int}%
   2.165 +\rulenamedx{card_Un_Int}%
   2.166  \isanewline
   2.167  \isanewline
   2.168  finite\ A\ \isasymLongrightarrow\ card\
   2.169  (Pow\ A)\  =\ 2\ \isacharcircum\ card\ A%
   2.170 -\rulename{card_Pow}%
   2.171 +\rulenamedx{card_Pow}%
   2.172  \isanewline
   2.173  \isanewline
   2.174  finite\ A\ \isasymLongrightarrow\isanewline
   2.175 @@ -449,7 +449,7 @@
   2.176  functions:
   2.177  \begin{isabelle}
   2.178  ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g
   2.179 -\rulename{ext}
   2.180 +\rulenamedx{ext}
   2.181  \end{isabelle}
   2.182  
   2.183  \indexbold{updating a function}%
   2.184 @@ -478,11 +478,11 @@
   2.185  defined:
   2.186  \begin{isabelle}%
   2.187  id\ \isasymequiv\ {\isasymlambda}x.\ x%
   2.188 -\rulename{id_def}\isanewline
   2.189 +\rulenamedx{id_def}\isanewline
   2.190  f\ \isasymcirc\ g\ \isasymequiv\
   2.191  {\isasymlambda}x.\ f\
   2.192  (g\ x)%
   2.193 -\rulename{o_def}
   2.194 +\rulenamedx{o_def}
   2.195  \end{isabelle}
   2.196  %
   2.197  Many familiar theorems concerning the identity and composition 
   2.198 @@ -500,12 +500,12 @@
   2.199  inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\
   2.200  {\isasymforall}y\isasymin  A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\
   2.201  =\ y%
   2.202 -\rulename{inj_on_def}\isanewline
   2.203 +\rulenamedx{inj_on_def}\isanewline
   2.204  surj\ f\ \isasymequiv\ {\isasymforall}y.\
   2.205  \isasymexists x.\ y\ =\ f\ x%
   2.206 -\rulename{surj_def}\isanewline
   2.207 +\rulenamedx{surj_def}\isanewline
   2.208  bij\ f\ \isasymequiv\ inj\ f\ \isasymand\ surj\ f
   2.209 -\rulename{bij_def}
   2.210 +\rulenamedx{bij_def}
   2.211  \end{isabelle}
   2.212  The second argument
   2.213  of \isa{inj_on} lets us express that a function is injective over a
   2.214 @@ -588,7 +588,7 @@
   2.215  \begin{isabelle}
   2.216  f\ `\ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin
   2.217  A.\ y\ =\ f\ x\isacharbraceright
   2.218 -\rulename{image_def}
   2.219 +\rulenamedx{image_def}
   2.220  \end{isabelle}
   2.221  %
   2.222  Here are some of the many facts proved about image: 
   2.223 @@ -637,7 +637,7 @@
   2.224  It is defined as follows: 
   2.225  \begin{isabelle}
   2.226  f\ -`\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright
   2.227 -\rulename{vimage_def}
   2.228 +\rulenamedx{vimage_def}
   2.229  \end{isabelle}
   2.230  %
   2.231  This is one of the facts proved about it:
   2.232 @@ -662,7 +662,7 @@
   2.233  definition: 
   2.234  \begin{isabelle}
   2.235  Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}%
   2.236 -\rulename{Id_def}
   2.237 +\rulenamedx{Id_def}
   2.238  \end{isabelle}
   2.239  
   2.240  \indexbold{composition!of relations}%
   2.241 @@ -670,7 +670,7 @@
   2.242  available: 
   2.243  \begin{isabelle}
   2.244  r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
   2.245 -\rulename{comp_def}
   2.246 +\rulenamedx{comp_def}
   2.247  \end{isabelle}
   2.248  %
   2.249  This is one of the many lemmas proved about these concepts: 
   2.250 @@ -698,7 +698,7 @@
   2.251  \begin{isabelle}
   2.252  ((a,b)\ \isasymin\ r\isasyminverse)\ =\
   2.253  ((b,a)\ \isasymin\ r)
   2.254 -\rulename{converse_iff}
   2.255 +\rulenamedx{converse_iff}
   2.256  \end{isabelle}
   2.257  %
   2.258  Here is a typical law proved about converse and composition: 
   2.259 @@ -713,7 +713,7 @@
   2.260  \begin{isabelle}
   2.261  (b\ \isasymin\ r\ ``\ A)\ =\ (\isasymexists x\isasymin
   2.262  A.\ (x,b)\ \isasymin\ r)
   2.263 -\rulename{Image_iff}
   2.264 +\rulenamedx{Image_iff}
   2.265  \end{isabelle}
   2.266  It satisfies many similar laws.
   2.267  
   2.268 @@ -724,13 +724,13 @@
   2.269  \begin{isabelle}
   2.270  (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\
   2.271  r)
   2.272 -\rulename{Domain_iff}%
   2.273 +\rulenamedx{Domain_iff}%
   2.274  \isanewline
   2.275  (a\ \isasymin\ Range\ r)\
   2.276  \ =\ (\isasymexists y.\
   2.277  (y,a)\
   2.278  \isasymin\ r)
   2.279 -\rulename{Range_iff}
   2.280 +\rulenamedx{Range_iff}
   2.281  \end{isabelle}
   2.282  
   2.283  Iterated composition of a relation is available.  The notation overloads 
   2.284 @@ -757,13 +757,13 @@
   2.285  rules:
   2.286  \begin{isabelle}
   2.287  (a,\ a)\ \isasymin \ r\isactrlsup *
   2.288 -\rulename{rtrancl_refl}\isanewline
   2.289 +\rulenamedx{rtrancl_refl}\isanewline
   2.290  p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup *
   2.291 -\rulename{r_into_rtrancl}\isanewline
   2.292 +\rulenamedx{r_into_rtrancl}\isanewline
   2.293  \isasymlbrakk (a,b)\ \isasymin \ r\isactrlsup *;\ 
   2.294  (b,c)\ \isasymin \ r\isactrlsup *\isasymrbrakk \ \isasymLongrightarrow \
   2.295  (a,c)\ \isasymin \ r\isactrlsup *
   2.296 -\rulename{rtrancl_trans}
   2.297 +\rulenamedx{rtrancl_trans}
   2.298  \end{isabelle}
   2.299  %
   2.300  Induction over the reflexive transitive closure is available: 
   2.301 @@ -785,9 +785,9 @@
   2.302  \isa{r\isacharcircum+}.  It has two  introduction rules: 
   2.303  \begin{isabelle}
   2.304  p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup +
   2.305 -\rulename{r_into_trancl}\isanewline
   2.306 +\rulenamedx{r_into_trancl}\isanewline
   2.307  \isasymlbrakk (a,\ b)\ \isasymin \ r\isactrlsup +;\ (b,\ c)\ \isasymin \ r\isactrlsup +\isasymrbrakk \ \isasymLongrightarrow \ (a,\ c)\ \isasymin \ r\isactrlsup +
   2.308 -\rulename{trancl_trans}
   2.309 +\rulenamedx{trancl_trans}
   2.310  \end{isabelle}
   2.311  %
   2.312  The induction rule resembles the one shown above. 
   2.313 @@ -910,7 +910,7 @@
   2.314  relation  behaves as expected and that it is well-founded: 
   2.315  \begin{isabelle}
   2.316  ((x,y)\ \isasymin\ less_than)\ =\ (x\ <\ y)
   2.317 -\rulename{less_than_iff}\isanewline
   2.318 +\rulenamedx{less_than_iff}\isanewline
   2.319  wf\ less_than
   2.320  \rulename{wf_less_than}
   2.321  \end{isabelle}
   2.322 @@ -925,7 +925,7 @@
   2.323  \begin{isabelle}
   2.324  inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\
   2.325  \isasymin\ r\isacharbraceright
   2.326 -\rulename{inv_image_def}\isanewline
   2.327 +\rulenamedx{inv_image_def}\isanewline
   2.328  wf\ r\ \isasymLongrightarrow\ wf\ (inv_image\ r\ f)
   2.329  \rulename{wf_inv_image}
   2.330  \end{isabelle}
   2.331 @@ -936,7 +936,7 @@
   2.332  \isa{measure} as shown: 
   2.333  \begin{isabelle}
   2.334  measure\ \isasymequiv\ inv_image\ less_than%
   2.335 -\rulename{measure_def}\isanewline
   2.336 +\rulenamedx{measure_def}\isanewline
   2.337  wf\ (measure\ f)
   2.338  \rulename{wf_measure}
   2.339  \end{isabelle}
   2.340 @@ -953,7 +953,7 @@
   2.341  \isasymor\isanewline
   2.342  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,a=a'\ \isasymand \ (b,b')\
   2.343  \isasymin \ rb\isacharbraceright 
   2.344 -\rulename{lex_prod_def}%
   2.345 +\rulenamedx{lex_prod_def}%
   2.346  \par\smallskip
   2.347  \isasymlbrakk wf\ ra;\ wf\ rb\isasymrbrakk \ \isasymLongrightarrow \ wf\ (ra\ <*lex*>\ rb)
   2.348  \rulename{wf_lex_prod}
   2.349 @@ -986,7 +986,7 @@
   2.350    {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
   2.351  \isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\
   2.352  \isasymLongrightarrow\ P\ a
   2.353 -\rulename{wf_induct}
   2.354 +\rulenamedx{wf_induct}
   2.355  \end{isabelle}
   2.356  Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded.
   2.357  
   2.358 @@ -1021,7 +1021,7 @@
   2.359  Isabelle's definition of monotone is overloaded over all orderings:
   2.360  \begin{isabelle}
   2.361  mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
   2.362 -\rulename{mono_def}
   2.363 +\rulenamedx{mono_def}
   2.364  \end{isabelle}
   2.365  %
   2.366  For fixed point operators, the ordering will be the subset relation: if