1.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Wed Feb 07 12:15:59 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Wed Feb 07 16:37:24 2001 +0100
     1.3 @@ -93,26 +93,26 @@
     1.4  
     1.5  text{*Relations.  transitive closure*}
     1.6  
     1.7 -lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*"
     1.8 +lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*"
     1.9  apply (erule rtrancl_induct)
    1.10  txt{*
    1.11  @{subgoals[display,indent=0,margin=65]}
    1.12  *};
    1.13   apply (rule rtrancl_refl)
    1.14 -apply (blast intro: r_into_rtrancl rtrancl_trans)
    1.15 +apply (blast intro: rtrancl_trans)
    1.16  done
    1.17  
    1.18  
    1.19 -lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*"
    1.20 +lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*"
    1.21  apply (erule rtrancl_induct)
    1.22   apply (rule rtrancl_refl)
    1.23 -apply (blast intro: r_into_rtrancl rtrancl_trans)
    1.24 +apply (blast intro: rtrancl_trans)
    1.25  done
    1.26  
    1.27 -lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    1.28 +lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
    1.29  by (auto intro: rtrancl_converseI dest: rtrancl_converseD)
    1.30  
    1.31 -lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
    1.32 +lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>"
    1.33  apply (intro equalityI subsetI)
    1.34  txt{*
    1.35  after intro rules