--- a/src/HOL/Hyperreal/Lim.ML Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML Tue Aug 07 16:36:52 2001 +0200
@@ -1294,7 +1294,7 @@
qed "NSDERIV_cmult_Id";
Addsimps [NSDERIV_cmult_Id];
-Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
by (induct_tac "n" 1);
by (dtac (DERIV_Id RS DERIV_mult) 2);
by (auto_tac (claset(),
@@ -1306,7 +1306,7 @@
qed "DERIV_pow";
(* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
qed "NSDERIV_pow";