| changeset 11868 | 56db9f3a6b3e |
| parent 11701 | 3d51fbf81c17 |
| child 12196 | a3be6b3a9c0b |
--- a/src/HOL/Integ/IntPower.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/IntPower.ML Mon Oct 22 11:54:22 2001 +0200 @@ -15,7 +15,7 @@ by (rtac (zmod_zmult_distrib RS sym) 1); qed "zpower_zmod"; -Goal "Numeral1^y = (Numeral1::int)"; +Goal "1^y = (1::int)"; by (induct_tac "y" 1); by Auto_tac; qed "zpower_1";