# HG changeset patch
# User huffman
# Date 1187630058 -7200
# Node ID eda777a2785b4a186608b1cfa44ab0898d38923f
# Parent  1e028d1140756a298ffc1bda7f0e27dc48cd4a90
use class instead of axclass

diff -r 1e028d114075 -r eda777a2785b src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Mon Aug 20 18:54:51 2007 +0200
+++ b/src/HOL/Word/BitSyntax.thy	Mon Aug 20 19:14:18 2007 +0200
@@ -12,18 +12,29 @@
 imports Main
 begin
 
-axclass bit < type
+class bit = type +
+  fixes bitNOT :: "'a \<Rightarrow> 'a"
+    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 
 text {*
   We want the bitwise operations to bind slightly weaker
   than @{text "+"} and @{text "-"}, but @{text "~~"} to 
   bind slightly stronger than @{text "*"}.
 *}
-consts
-  bitNOT  :: "'a::bit \<Rightarrow> 'a"       ("NOT _" [70] 71)
-  bitAND  :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
-  bitOR   :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)
-  bitXOR  :: "'a::bit \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
+
+notation
+  bitNOT  ("NOT _" [70] 71)
+
+notation
+  bitAND  (infixr "AND" 64)
+
+notation
+  bitOR   (infixr "OR"  59)
+
+notation
+  bitXOR  (infixr "XOR" 59)
 
 text {*
   Testing and shifting operations.
@@ -40,13 +51,12 @@
 
 subsection {* Bitwise operations on type @{typ bit} *}
 
-instance bit :: bit ..
-
-defs (overloaded)
+instance bit :: bit
   NOT_bit_def: "NOT x \<equiv> case x of bit.B0 \<Rightarrow> bit.B1 | bit.B1 \<Rightarrow> bit.B0"
   AND_bit_def: "x AND y \<equiv> case x of bit.B0 \<Rightarrow> bit.B0 | bit.B1 \<Rightarrow> y"
   OR_bit_def: "x OR y :: bit \<equiv> NOT (NOT x AND NOT y)"
   XOR_bit_def: "x XOR y :: bit \<equiv> (x AND NOT y) OR (NOT x AND y)"
+  ..
 
 lemma bit_simps [simp]:
   "NOT bit.B0 = bit.B1"