src/HOL/Library/Word.thy

 (*  Title:      HOL/Library/Word.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
 header {* Binary Words *}
 

 
 datatype bit =
     Zero ("\<zero>")
   | One ("\<one>")
 
-primrec
-  bitval :: "bit => nat"
-where
-  "bitval \<zero> = 0"
+primrec bitval :: "bit => nat" where
+    "bitval \<zero> = 0"
   | "bitval \<one> = 1"
 
 consts
   bitnot :: "bit => bit"
   bitand :: "bit => bit => bit" (infixr "bitand" 35)

   proof -
     from lw
     show ?thesis
       apply simp
       apply (subst power_Suc [symmetric])
-      apply (simp del: power_int.simps)
+      apply simp
       done
   qed
   finally show ?thesis .
 qed