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"
```