src/HOL/Complex/NSInduct.ML
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
     1.1 --- a/src/HOL/Complex/NSInduct.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSInduct.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -11,8 +11,8 @@
     1.4  by (Ultra_tac 1);
     1.5  qed "starPNat";
     1.6  
     1.7 -Goalw [hypnat_of_nat_def] "( *pNat* P) (hypnat_of_nat n) = P n";
     1.8 -by (auto_tac (claset(),simpset() addsimps [starPNat]));
     1.9 +Goal "( *pNat* P) (hypnat_of_nat n) = P n";
    1.10 +by (auto_tac (claset(),simpset() addsimps [starPNat, hypnat_of_nat_eq]));
    1.11  qed "starPNat_hypnat_of_nat";
    1.12  Addsimps [starPNat_hypnat_of_nat];
    1.13  
    1.14 @@ -27,7 +27,7 @@
    1.15  by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
    1.16  by (rtac ccontr 1);
    1.17  by (auto_tac (claset(),simpset() addsimps [starPNat,
    1.18 -    hypnat_of_nat_def,hypnat_add]));
    1.19 +    hypnat_of_nat_eq,hypnat_add]));
    1.20  qed "hypnat_induct_obj";
    1.21  
    1.22  Goal