src/HOL/Hyperreal/Lim.ML
changeset 11468 02cd5d5bc497
parent 11383 297625089e80
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Hyperreal/Lim.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -1294,7 +1294,7 @@
     1.4  qed "NSDERIV_cmult_Id";
     1.5  Addsimps [NSDERIV_cmult_Id];
     1.6  
     1.7 -Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
     1.8 +Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
     1.9  by (induct_tac "n" 1);
    1.10  by (dtac (DERIV_Id RS DERIV_mult) 2);
    1.11  by (auto_tac (claset(), 
    1.12 @@ -1306,7 +1306,7 @@
    1.13  qed "DERIV_pow";
    1.14  
    1.15  (* NS version *)
    1.16 -Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
    1.17 +Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
    1.18  by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
    1.19  qed "NSDERIV_pow";
    1.20