src/HOL/Bali/Basis.thy

 lemma rtrancl_into_rtrancl2: 
   "\<lbrakk> (a, b) \<in>  r; (b, c) \<in> r^* \<rbrakk> \<Longrightarrow> (a, c) \<in>  r^*"
 by (auto intro: r_into_rtrancl rtrancl_trans)
 
 lemma triangle_lemma:
- "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r*; (a,y)\<in>r*\<rbrakk> 
- \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
+ "\<lbrakk> \<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c; (a,x)\<in>r\<^sup>*; (a,y)\<in>r\<^sup>*\<rbrakk> 
+ \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
 proof -
   note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
   note converse_rtranclE = converse_rtranclE [consumes 1] 
   assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
-  assume "(a,x)\<in>r*" 
-  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
+  assume "(a,x)\<in>r\<^sup>*" 
+  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
   proof (induct rule: converse_rtrancl_induct)
-    assume "(x,y)\<in>r*"
+    assume "(x,y)\<in>r\<^sup>*"
     then show ?thesis 
       by blast
   next
     fix a v
     assume a_v_r: "(a, v) \<in> r" and
-          v_x_rt: "(v, x) \<in> r*" and
-          a_y_rt: "(a, y) \<in> r*"  and
-             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
+          v_x_rt: "(v, x) \<in> r\<^sup>*" and
+          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
+             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
     from a_y_rt 
-    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
+    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
     proof (cases rule: converse_rtranclE)
       assume "a=y"
-      with a_v_r v_x_rt have "(y,x) \<in> r*"
+      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
 	by (auto intro: r_into_rtrancl rtrancl_trans)
       then show ?thesis 
 	by blast
     next
       fix w 
       assume a_w_r: "(a, w) \<in> r" and
-            w_y_rt: "(w, y) \<in> r*"
+            w_y_rt: "(w, y) \<in> r\<^sup>*"
       from a_v_r a_w_r unique 
       have "v=w" 
 	by auto
       with w_y_rt hyp 
       show ?thesis

   qed
 qed
 
 
 lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
- "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+ "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 apply (erule rtranclE)
 apply (auto dest: rtrancl_into_trancl1)
 done
 
 (* ### To Transitive_Closure *)