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.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);