--- 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: