--- a/src/HOL/Word/Bit_Operations.thy Sun Aug 18 13:58:33 2013 +0200
+++ b/src/HOL/Word/Bit_Operations.thy Sun Aug 18 15:29:50 2013 +0200
@@ -8,6 +8,8 @@
imports "~~/src/HOL/Library/Bit"
begin
+subsection {* Abstract syntactic bit operations *}
+
class bit =
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
@@ -35,7 +37,7 @@
class bitss = bits +
fixes msb :: "'a \<Rightarrow> bool"
-
+
subsection {* Bitwise operations on @{typ bit} *}
instantiation bit :: bit