src/HOL/Bali/Basis.thy
changeset 32960 69916a850301
parent 32376 66b4946d9483
child 33965 f57c11db4ad4
     1.1 --- a/src/HOL/Bali/Basis.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/Basis.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -86,19 +86,19 @@
     1.4      proof (cases rule: converse_rtranclE)
     1.5        assume "a=y"
     1.6        with a_v_r v_x_rt have "(y,x) \<in> r\<^sup>*"
     1.7 -	by (auto intro: r_into_rtrancl rtrancl_trans)
     1.8 +        by (auto intro: r_into_rtrancl rtrancl_trans)
     1.9        then show ?thesis 
    1.10 -	by blast
    1.11 +        by blast
    1.12      next
    1.13        fix w 
    1.14        assume a_w_r: "(a, w) \<in> r" and
    1.15              w_y_rt: "(w, y) \<in> r\<^sup>*"
    1.16        from a_v_r a_w_r unique 
    1.17        have "v=w" 
    1.18 -	by auto
    1.19 +        by auto
    1.20        with w_y_rt hyp 
    1.21        show ?thesis
    1.22 -	by blast
    1.23 +        by blast
    1.24      qed
    1.25    qed
    1.26  qed
    1.27 @@ -213,11 +213,11 @@
    1.28  primrec  "the_In3 (In3 c) = c"
    1.29  
    1.30  syntax
    1.31 -	 In1l	:: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    1.32 -	 In1r	:: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    1.33 +         In1l   :: "'al \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    1.34 +         In1r   :: "'ar \<Rightarrow> ('al + 'ar, 'b, 'c) sum3"
    1.35  translations
    1.36 -	"In1l e" == "In1 (Inl e)"
    1.37 -	"In1r c" == "In1 (Inr c)"
    1.38 +        "In1l e" == "In1 (Inl e)"
    1.39 +        "In1r c" == "In1 (Inr c)"
    1.40  
    1.41  syntax the_In1l :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'al"
    1.42         the_In1r :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> 'ar"