1.1 --- a/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:10 2009 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Aug 13 17:19:42 2009 +0100
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  theory Basis imports Main begin
     1.6  
     1.7 -declare [[unify_search_bound = 40, unify_trace_bound = 40]]
     1.8 -
     1.9  
    1.10  section "misc"
    1.11  
    1.12 @@ -65,36 +63,36 @@
    1.13  by (auto intro: r_into_rtrancl rtrancl_trans)
    1.14  
    1.15  lemma triangle_lemma:
    1.16 - "\<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> 
    1.17 - \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.18 + "\<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> 
    1.19 + \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
    1.20  proof -
    1.21    note converse_rtrancl_induct = converse_rtrancl_induct [consumes 1]
    1.22    note converse_rtranclE = converse_rtranclE [consumes 1] 
    1.23    assume unique: "\<And> a b c. \<lbrakk>(a,b)\<in>r; (a,c)\<in>r\<rbrakk> \<Longrightarrow> b=c"
    1.24 -  assume "(a,x)\<in>r\<^sup>*" 
    1.25 -  then show "(a,y)\<in>r\<^sup>* \<Longrightarrow> (x,y)\<in>r\<^sup>* \<or> (y,x)\<in>r\<^sup>*"
    1.26 +  assume "(a,x)\<in>r*" 
    1.27 +  then show "(a,y)\<in>r* \<Longrightarrow> (x,y)\<in>r* \<or> (y,x)\<in>r*"
    1.28    proof (induct rule: converse_rtrancl_induct)
    1.29 -    assume "(x,y)\<in>r\<^sup>*"
    1.30 +    assume "(x,y)\<in>r*"
    1.31      then show ?thesis 
    1.32        by blast
    1.33    next
    1.34      fix a v
    1.35      assume a_v_r: "(a, v) \<in> r" and
    1.36 -          v_x_rt: "(v, x) \<in> r\<^sup>*" and
    1.37 -          a_y_rt: "(a, y) \<in> r\<^sup>*"  and
    1.38 -             hyp: "(v, y) \<in> r\<^sup>* \<Longrightarrow> (x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    1.39 +          v_x_rt: "(v, x) \<in> r*" and
    1.40 +          a_y_rt: "(a, y) \<in> r*"  and
    1.41 +             hyp: "(v, y) \<in> r* \<Longrightarrow> (x, y) \<in> r* \<or> (y, x) \<in> r*"
    1.42      from a_y_rt 
    1.43 -    show "(x, y) \<in> r\<^sup>* \<or> (y, x) \<in> r\<^sup>*"
    1.44 +    show "(x, y) \<in> r* \<or> (y, x) \<in> r*"
    1.45      proof (cases rule: converse_rtranclE)
    1.46        assume "a=y"
    1.47 -      with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
    1.48 +      with a_v_r v_x_rt have "(y,x) \<in> r*"
    1.49  	by (auto intro: r_into_rtrancl rtrancl_trans)
    1.50        then show ?thesis 
    1.51  	by blast
    1.52      next
    1.53        fix w 
    1.54        assume a_w_r: "(a, w) \<in> r" and
    1.55 -            w_y_rt: "(w, y) \<in> r\<^sup>*"
    1.56 +            w_y_rt: "(w, y) \<in> r*"
    1.57        from a_v_r a_w_r unique 
    1.58        have "v=w" 
    1.59  	by auto
    1.60 @@ -107,7 +105,7 @@
    1.61  
    1.62  
    1.63  lemma rtrancl_cases [consumes 1, case_names Refl Trancl]:
    1.64 - "\<lbrakk>(a,b)\<in>r\<^sup>*;  a = b \<Longrightarrow> P; (a,b)\<in>r\<^sup>+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.65 + "\<lbrakk>(a,b)\<in>r*;  a = b \<Longrightarrow> P; (a,b)\<in>r+ \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.66  apply (erule rtranclE)
    1.67  apply (auto dest: rtrancl_into_trancl1)
    1.68  done