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.7 -    by transfer (simp add: add_ac realrel_def)
     1.8 +    by transfer (simp add: ac_simps realrel_def)
     1.9    show "(a + b) + c = a + (b + c)"
    1.10 -    by transfer (simp add: add_ac realrel_def)
    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)
    1.34 -apply (simp add: diff_le_eq add_ac)
    1.35 +apply (simp add: diff_le_eq ac_simps)
    1.36  done
    1.37  
    1.38  lemma le_RealI: