src/HOL/Complex/NSCA.thy
changeset 15013 34264f5e4691
parent 14653 0848ab6fe5fc
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Complex/NSCA.thy	Wed Jun 30 14:04:58 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Jul 01 12:29:53 2004 +0200
     1.3 @@ -508,7 +508,7 @@
     1.4  lemma capprox_SComplex_mult_cancel_zero:
     1.5       "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
     1.6  apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
     1.7 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
     1.8 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
     1.9  done
    1.10  
    1.11  lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
    1.12 @@ -524,7 +524,7 @@
    1.13  lemma capprox_SComplex_mult_cancel:
    1.14       "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
    1.15  apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
    1.16 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
    1.17 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
    1.18  done
    1.19  
    1.20  lemma capprox_SComplex_mult_cancel_iff1 [simp]:
    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 hcomplex_mult_assoc)
    1.26 +apply (simp add: divide_inverse mult_assoc)
    1.27  done
    1.28  
    1.29  lemma SComplex_capprox_iff:
    1.30 @@ -901,10 +901,11 @@
    1.31  apply (drule CFinite_inverse2)+
    1.32  apply (drule capprox_mult2, assumption, auto)
    1.33  apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
    1.34 -apply (auto intro: capprox_sym simp add: hcomplex_mult_assoc)
    1.35 +apply (auto intro: capprox_sym simp add: mult_assoc)
    1.36  done
    1.37  
    1.38 -lemmas hcomplex_of_complex_capprox_inverse =  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
    1.39 +lemmas hcomplex_of_complex_capprox_inverse =
    1.40 +  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
    1.41  
    1.42  lemma inverse_add_CInfinitesimal_capprox:
    1.43       "[| x \<in> CFinite - CInfinitesimal;  
    1.44 @@ -935,7 +936,7 @@
    1.45  apply safe
    1.46  apply (frule CFinite_inverse, assumption)
    1.47  apply (drule not_CInfinitesimal_not_zero)
    1.48 -apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
    1.49 +apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
    1.50  done
    1.51  
    1.52  lemma capprox_CFinite_mult_cancel_iff1: