# HG changeset patch
# User wenzelm
# Date 1334674117 -7200
# Node ID 85c6268b4071cf5a77e14837d214cf1fe30f4d96
# Parent  d52da3e7aa4cc199e2a67bbda87b27a59a75698d
updated rel_comp ~> relcomp (cf. e1b761c216ac);

diff -r d52da3e7aa4c -r 85c6268b4071 doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Tue Apr 17 15:25:43 2012 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy	Tue Apr 17 16:48:37 2012 +0200
@@ -11,8 +11,8 @@
 *}
 
 text{*
-@{thm[display] rel_comp_def[no_vars]}
-\rulename{rel_comp_def}
+@{thm[display] relcomp_unfold[no_vars]}
+\rulename{relcomp_unfold}
 *}
 
 text{*
@@ -21,8 +21,8 @@
 *}
 
 text{*
-@{thm[display] rel_comp_mono[no_vars]}
-\rulename{rel_comp_mono}
+@{thm[display] relcomp_mono[no_vars]}
+\rulename{relcomp_mono}
 *}
 
 text{*
@@ -31,8 +31,8 @@
 *}
 
 text{*
-@{thm[display] converse_rel_comp[no_vars]}
-\rulename{converse_rel_comp}
+@{thm[display] converse_relcomp[no_vars]}
+\rulename{converse_relcomp}
 *}
 
 text{*