diff -r 83acab8042ad -r c92e38c3cbaa doc-src/TutorialI/Sets/sets.tex
--- 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}%