src/HOL/Hyperreal/HTranscendental.ML

 Addsimps [hypreal_sqrt_hrabs2];
 
 Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 by (auto_tac (claset(),simpset() addsimps [starfun,
-    hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
+    hypreal_hrabs,hypnat_of_nat_eq,hyperpow]));
 qed "hypreal_sqrt_hyperpow_hrabs";
 Addsimps [hypreal_sqrt_hyperpow_hrabs];
 
 Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
 by (res_inst_tac [("n","1")] power_inject_base 1);