1.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:07 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Thu Dec 13 16:48:34 2001 +0100
     1.3 @@ -12,8 +12,8 @@
     1.4  *}
     1.5  
     1.6  text{*
     1.7 -@{thm[display] comp_def[no_vars]}
     1.8 -\rulename{comp_def}
     1.9 +@{thm[display] rel_comp_def[no_vars]}
    1.10 +\rulename{rel_comp_def}
    1.11  *}
    1.12  
    1.13  text{*
    1.14 @@ -22,8 +22,8 @@
    1.15  *}
    1.16  
    1.17  text{*
    1.18 -@{thm[display] comp_mono[no_vars]}
    1.19 -\rulename{comp_mono}
    1.20 +@{thm[display] rel_comp_mono[no_vars]}
    1.21 +\rulename{rel_comp_mono}
    1.22  *}
    1.23  
    1.24  text{*
    1.25 @@ -32,8 +32,8 @@
    1.26  *}
    1.27  
    1.28  text{*
    1.29 -@{thm[display] converse_comp[no_vars]}
    1.30 -\rulename{converse_comp}
    1.31 +@{thm[display] converse_rel_comp[no_vars]}
    1.32 +\rulename{converse_rel_comp}
    1.33  *}
    1.34  
    1.35  text{*