src/HOL/Complex/NSComplexBin.ML
changeset 14320 fb7a114826be
parent 14318 7dbd3988b15b
child 14335 9c0b5e081037
     1.1 --- a/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:23 2003 +0100
     1.2 +++ b/src/HOL/Complex/NSComplexBin.ML	Tue Dec 23 14:45:47 2003 +0100
     1.3 @@ -24,11 +24,11 @@
     1.4  qed "hcomplex_hypreal_number_of";
     1.5  
     1.6  Goalw [hcomplex_number_of_def] "Numeral0 = (0::hcomplex)";
     1.7 -by (simp_tac (simpset() addsimps [hcomplex_of_complex_zero RS sym]) 1);
     1.8 +by(Simp_tac 1);
     1.9  qed "hcomplex_numeral_0_eq_0";
    1.10  
    1.11  Goalw [hcomplex_number_of_def] "Numeral1 = (1::hcomplex)";
    1.12 -by (simp_tac (simpset() addsimps [hcomplex_of_complex_one RS sym]) 1);
    1.13 +by(Simp_tac 1);
    1.14  qed "hcomplex_numeral_1_eq_1";
    1.15  
    1.16  (*