diff -r 1d6d2ce2ad3e -r fb6ef69b8c85 src/Doc/Tutorial/document/sets.tex
--- a/src/Doc/Tutorial/document/sets.tex	Tue Oct 15 12:25:45 2013 +0200
+++ b/src/Doc/Tutorial/document/sets.tex	Tue Oct 15 11:49:39 2013 +0100
@@ -660,8 +660,8 @@
 \textbf{Composition} of relations (the infix \sdx{O}) is also
 available: 
 \begin{isabelle}
-r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
-\rulenamedx{relcomp_def}
+r\ O\ s\ = \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
+\rulenamedx{relcomp_unfold}
 \end{isabelle}
 %
 This is one of the many lemmas proved about these concepts: