--- 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 =