| changeset 11701 | 3d51fbf81c17 |
| parent 9509 | 0f3ee1f89ca8 |
| child 11868 | 56db9f3a6b3e |
--- a/src/HOL/Integ/IntPower.ML Fri Oct 05 21:50:37 2001 +0200 +++ b/src/HOL/Integ/IntPower.ML Fri Oct 05 21:52:39 2001 +0200 @@ -15,7 +15,7 @@ by (rtac (zmod_zmult_distrib RS sym) 1); qed "zpower_zmod"; -Goal "#1^y = (#1::int)"; +Goal "Numeral1^y = (Numeral1::int)"; by (induct_tac "y" 1); by Auto_tac; qed "zpower_1";