updated rel_comp ~> relcomp (cf. e1b761c216ac);
authorwenzelm
Tue, 17 Apr 2012 16:48:37 +0200
changeset 47508 85c6268b4071
parent 47507 d52da3e7aa4c
child 47509 6f215c2ebd72
updated rel_comp ~> relcomp (cf. e1b761c216ac);
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{*