src/HOL/Real.thy
 changeset 57514 bdc2c6b40bf2 parent 57512 cc97b347b301 child 58040 9a867afaab5a
```     1.1 --- a/src/HOL/Real.thy	Sat Jul 05 10:09:01 2014 +0200
1.2 +++ b/src/HOL/Real.thy	Sat Jul 05 11:01:53 2014 +0200
1.3 @@ -474,9 +474,9 @@
1.4  instance proof
1.5    fix a b c :: real
1.6    show "a + b = b + a"
1.8 +    by transfer (simp add: ac_simps realrel_def)
1.9    show "(a + b) + c = a + (b + c)"
1.11 +    by transfer (simp add: ac_simps realrel_def)
1.12    show "0 + a = a"
1.13      by transfer (simp add: realrel_def)
1.14    show "- a + a = 0"
1.15 @@ -484,11 +484,11 @@
1.16    show "a - b = a + - b"
1.17      by (rule minus_real_def)
1.18    show "(a * b) * c = a * (b * c)"
1.19 -    by transfer (simp add: mult_ac realrel_def)
1.20 +    by transfer (simp add: ac_simps realrel_def)
1.21    show "a * b = b * a"
1.22 -    by transfer (simp add: mult_ac realrel_def)
1.23 +    by transfer (simp add: ac_simps realrel_def)
1.24    show "1 * a = a"
1.25 -    by transfer (simp add: mult_ac realrel_def)
1.26 +    by transfer (simp add: ac_simps realrel_def)
1.27    show "(a + b) * c = a * c + b * c"
1.28      by transfer (simp add: distrib_right realrel_def)
1.29    show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
1.30 @@ -707,7 +707,7 @@
1.31    shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
1.32  unfolding not_less [symmetric, where 'a=real] less_real_def
1.33  apply (simp add: diff_Real not_positive_Real X Y)