--- a/doc-src/TutorialI/Sets/sets.tex Thu Dec 13 16:48:07 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Dec 13 16:48:34 2001 +0100
@@ -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
-\rulenamedx{comp_def}
+\rulenamedx{rel_comp_def}
\end{isabelle}
%
This is one of the many lemmas proved about these concepts:
@@ -686,7 +686,7 @@
\isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\
\isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\
s\isacharprime\ \isasymsubseteq\ r\ O\ s%
-\rulename{comp_mono}
+\rulename{rel_comp_mono}
\end{isabelle}
\indexbold{converse!of a relation}%
@@ -704,7 +704,7 @@
Here is a typical law proved about converse and composition:
\begin{isabelle}
(r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse
-\rulename{converse_comp}
+\rulename{converse_rel_comp}
\end{isabelle}
\indexbold{image!under a relation}%