src/HOL/Library/Abstract_Rat.thy
 changeset 32960 69916a850301 parent 32456 341c83339aeb child 33657 a4179bf442d1
```     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -56,18 +56,18 @@
1.4      moreover
1.5      {assume b: "b > 0"
1.6        from b have "?b' \<ge> 0"
1.7 -	by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
1.8 +        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
1.9        with nz' have b': "?b' > 0" by arith
1.10        from b b' anz bnz nz' gp1 have ?thesis
1.11 -	by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
1.12 +        by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
1.13      moreover {assume b: "b < 0"
1.14        {assume b': "?b' \<ge> 0"
1.15 -	from gpos have th: "?g \<ge> 0" by arith
1.16 -	from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
1.17 -	have False using b by arith }
1.18 +        from gpos have th: "?g \<ge> 0" by arith
1.19 +        from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
1.20 +        have False using b by arith }
1.21        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
1.22        from anz bnz nz' b b' gp1 have ?thesis
1.23 -	by (simp add: isnormNum_def normNum_def Let_def split_def)}
1.24 +        by (simp add: isnormNum_def normNum_def Let_def split_def)}
1.25      ultimately have ?thesis by blast
1.26    }
1.27    ultimately show ?thesis by blast
1.28 @@ -287,14 +287,14 @@
1.29        hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z"  by (simp add:add_divide_distrib)
1.30        hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp
1.31        from z aa' bb' have ?thesis
1.34      moreover {assume z: "a * b' + b * a' \<noteq> 0"
1.35        let ?g = "gcd (a * b' + b * a') (b*b')"
1.36        have gz: "?g \<noteq> 0" using z by simp
1.37        have ?thesis using aa' bb' z gz
1.38 -	of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]	of_int_div[where ?'a = 'a,
1.39 -	OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]