# HG changeset patch
# User nipkow
# Date 1381832745 -7200
# Node ID 1d6d2ce2ad3eb098059dd14dbff277955f672c85
# Parent  80660c529d7487b14c70b0dca26f66356827c150
fixed thm names

diff -r 80660c529d74 -r 1d6d2ce2ad3e src/Doc/Tutorial/document/sets.tex
--- a/src/Doc/Tutorial/document/sets.tex	Tue Oct 15 10:59:34 2013 +0200
+++ b/src/Doc/Tutorial/document/sets.tex	Tue Oct 15 12:25:45 2013 +0200
@@ -661,7 +661,7 @@
 available: 
 \begin{isabelle}
 r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright
-\rulenamedx{rel_comp_def}
+\rulenamedx{relcomp_def}
 \end{isabelle}
 %
 This is one of the many lemmas proved about these concepts: 
@@ -677,7 +677,7 @@
 \isasymlbrakk r\isacharprime\ \isasymsubseteq\ r;\ s\isacharprime\
 \isasymsubseteq\ s\isasymrbrakk\ \isasymLongrightarrow\ r\isacharprime\ O\
 s\isacharprime\ \isasymsubseteq\ r\ O\ s%
-\rulename{rel_comp_mono}
+\rulename{relcomp_mono}
 \end{isabelle}
 
 \indexbold{converse!of a relation}%
@@ -695,7 +695,7 @@
 Here is a typical law proved about converse and composition: 
 \begin{isabelle}
 (r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse
-\rulename{converse_rel_comp}
+\rulename{converse_relcomp}
 \end{isabelle}
 
 \indexbold{image!under a relation}%