src/HOL/Complex/NSCA.thy
changeset 14430 5cb24165a2e1
parent 14408 0cc42bb96330
child 14469 c7674b7034f5
     1.1 --- a/src/HOL/Complex/NSCA.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4  done
     1.5  
     1.6  lemma SComplex_divide: "[| x \<in> SComplex;  y \<in> SComplex |] ==> x/y \<in> SComplex"
     1.7 -by (simp add: SComplex_mult SComplex_inverse divide_inverse_zero)
     1.8 +by (simp add: SComplex_mult SComplex_inverse divide_inverse)
     1.9  
    1.10  lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
    1.11  apply (simp add: SComplex_def)
    1.12 @@ -98,7 +98,7 @@
    1.13  
    1.14  lemma SComplex_divide_number_of:
    1.15       "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
    1.16 -apply (simp only: divide_inverse_zero)
    1.17 +apply (simp only: divide_inverse)
    1.18  apply (blast intro!: SComplex_number_of SComplex_mult SComplex_inverse)
    1.19  done
    1.20  
    1.21 @@ -618,7 +618,7 @@
    1.22  lemma CInfinitesimal_ratio:
    1.23       "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
    1.24  apply (drule CInfinitesimal_CFinite_mult2, assumption)
    1.25 -apply (simp add: divide_inverse_zero hcomplex_mult_assoc)
    1.26 +apply (simp add: divide_inverse hcomplex_mult_assoc)
    1.27  done
    1.28  
    1.29  lemma SComplex_capprox_iff:
    1.30 @@ -1126,7 +1126,7 @@
    1.31  lemma stc_divide [simp]:
    1.32       "[| x \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]  
    1.33        ==> stc(x/y) = (stc x) / (stc y)"
    1.34 -by (simp add: divide_inverse_zero stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
    1.35 +by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse)
    1.36  
    1.37  lemma stc_idempotent [simp]: "x \<in> CFinite ==> stc(stc(x)) = stc(x)"
    1.38  by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)