--- a/src/HOL/Integ/IntPower.thy Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Integ/IntPower.thy Fri Oct 05 21:52:39 2001 +0200
@@ -12,7 +12,7 @@
int :: {power}
primrec
- power_0 "p ^ 0 = #1"
+ power_0 "p ^ 0 = Numeral1"
power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
end