src/HOL/Real.thy
changeset 54230 b1d955791529
parent 53652 18fbca265e2e
child 54258 adfc759263ab
     1.1 --- a/src/HOL/Real.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Real.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  lemma vanishes_diff:
     1.5    assumes X: "vanishes X" and Y: "vanishes Y"
     1.6    shows "vanishes (\<lambda>n. X n - Y n)"
     1.7 -unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
     1.8 +  unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y)
     1.9  
    1.10  lemma vanishes_mult_bounded:
    1.11    assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
    1.12 @@ -170,7 +170,7 @@
    1.13  lemma cauchy_diff [simp]:
    1.14    assumes X: "cauchy X" and Y: "cauchy Y"
    1.15    shows "cauchy (\<lambda>n. X n - Y n)"
    1.16 -using assms unfolding diff_minus by simp
    1.17 +  using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff)
    1.18  
    1.19  lemma cauchy_imp_bounded:
    1.20    assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
    1.21 @@ -456,7 +456,7 @@
    1.22  lemma diff_Real:
    1.23    assumes X: "cauchy X" and Y: "cauchy Y"
    1.24    shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
    1.25 -  unfolding minus_real_def diff_minus
    1.26 +  unfolding minus_real_def
    1.27    by (simp add: minus_Real add_Real X Y)
    1.28  
    1.29  lemma mult_Real:
    1.30 @@ -607,7 +607,7 @@
    1.31      unfolding less_eq_real_def less_real_def
    1.32      by (auto, drule (1) positive_add, simp add: positive_zero)
    1.33    show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
    1.34 -    unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
    1.35 +    unfolding less_eq_real_def less_real_def by auto
    1.36      (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
    1.37      (* Should produce c + b - (c + a) \<equiv> b - a *)
    1.38    show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"