src/HOL/Complex/ComplexArith0.ML
changeset 14373 67a628beb981
parent 14348 744c868ee0b7
     1.1 --- a/src/HOL/Complex/ComplexArith0.ML	Tue Feb 03 10:19:21 2004 +0100
     1.2 +++ b/src/HOL/Complex/ComplexArith0.ML	Tue Feb 03 11:06:36 2004 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val trans_tac         = Real_Numeral_Simprocs.trans_tac
     1.5    val norm_tac =  ALLGOALS (simp_tac (HOL_ss addsimps complex_minus_from_mult_simps @ mult_1s)) 
     1.6                    THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@complex_mult_minus_simps))
     1.7 -                  THEN ALLGOALS (simp_tac (HOL_ss addsimps complex_mult_ac))
     1.8 +                  THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
     1.9    val numeral_simp_tac	=  ALLGOALS (simp_tac (HOL_ss addsimps rel_complex_number_of@bin_simps))
    1.10    val simplify_meta_eq  = simplify_meta_eq
    1.11    end
    1.12 @@ -105,7 +105,7 @@
    1.13    val dest_coeff	= dest_coeff
    1.14    val find_first	= find_first []
    1.15    val trans_tac         = Real_Numeral_Simprocs.trans_tac
    1.16 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@complex_mult_ac))
    1.17 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    1.18    end;
    1.19  
    1.20  
    1.21 @@ -173,13 +173,13 @@
    1.22  Addsimps [complex_minus1_divide];
    1.23  
    1.24  Goal "(x + - a = (0::complex)) = (x=a)";
    1.25 -by (simp_tac (simpset() addsimps [complex_diff_eq_eq,symmetric complex_diff_def]) 1);
    1.26 +by (simp_tac (simpset() addsimps [diff_eq_eq,symmetric complex_diff_def]) 1);
    1.27  qed "complex_add_minus_iff";
    1.28  Addsimps [complex_add_minus_iff];
    1.29  
    1.30  Goal "(x+y = (0::complex)) = (y = -x)";
    1.31  by Auto_tac;
    1.32 -by (dtac (sym RS (complex_diff_eq_eq RS iffD2)) 1);
    1.33 +by (dtac (sym RS (diff_eq_eq RS iffD2)) 1);
    1.34  by Auto_tac;  
    1.35  qed "complex_add_eq_0_iff";
    1.36  AddIffs [complex_add_eq_0_iff];