--- a/src/HOL/Library/Word.thy Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Library/Word.thy Fri Jan 25 14:53:52 2008 +0100
@@ -40,11 +40,11 @@
Zero ("\<zero>")
| One ("\<one>")
-consts
+primrec
bitval :: "bit => nat"
-primrec
+where
"bitval \<zero> = 0"
- "bitval \<one> = 1"
+ | "bitval \<one> = 1"
consts
bitnot :: "bit => bit"
@@ -1531,7 +1531,7 @@
show ?thesis
apply simp
apply (subst power_Suc [symmetric])
- apply (simp del: power.simps)
+ apply (simp del: power_int.simps)
done
qed
finally show ?thesis .