diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Integ/Numeral.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -51,6 +51,8 @@
 
 abbreviation
   "Numeral0 \<equiv> number_of Pls"
+
+abbreviation
   "Numeral1 \<equiv> number_of (Pls BIT B1)"
 
 lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
@@ -64,9 +66,11 @@
   unfolding Let_def ..
 
 definition
-  succ :: "int \<Rightarrow> int"
+  succ :: "int \<Rightarrow> int" where
   "succ k = k + 1"
-  pred :: "int \<Rightarrow> int"
+
+definition
+  pred :: "int \<Rightarrow> int" where
   "pred k = k - 1"
 
 lemmas numeral_simps =