src/HOL/NSA/HTranscendental.thy
changeset 37887 2ae085b07f2f
parent 31271 0237e5e40b71
child 44316 84b6f7a6cea4
     1.1 --- a/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/NSA/HTranscendental.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -258,7 +258,7 @@
     1.4              simp add: mult_assoc)
     1.5  apply (rule approx_add_right_cancel [where d="-1"])
     1.6  apply (rule approx_sym [THEN [2] approx_trans2])
     1.7 -apply (auto simp add: diff_def mem_infmal_iff)
     1.8 +apply (auto simp add: diff_minus mem_infmal_iff)
     1.9  done
    1.10  
    1.11  lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
    1.12 @@ -450,7 +450,7 @@
    1.13  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
    1.14              simp add: mult_assoc)
    1.15  apply (rule approx_add_right_cancel [where d = "-1"])
    1.16 -apply (simp add: diff_def)
    1.17 +apply (simp add: diff_minus)
    1.18  done
    1.19  
    1.20  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"