src/HOL/Hyperreal/HTranscendental.ML
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4  Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
     1.5  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
     1.6  by (auto_tac (claset(),simpset() addsimps [starfun,
     1.7 -    hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
     1.8 +    hypreal_hrabs,hypnat_of_nat_eq,hyperpow]));
     1.9  qed "hypreal_sqrt_hyperpow_hrabs";
    1.10  Addsimps [hypreal_sqrt_hyperpow_hrabs];
    1.11