src/HOL/Hyperreal/HyperPow.ML
changeset 11468 02cd5d5bc497
parent 11377 0f16ad464c62
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
     1.5  qed "hrealpow_add";
     1.6  
     1.7 -Goal "(r::hypreal) ^ 1 = r";
     1.8 +Goal "(r::hypreal) ^ 1' = r";
     1.9  by (Simp_tac 1);
    1.10  qed "hrealpow_one";
    1.11  Addsimps [hrealpow_one];