--- a/src/HOL/Word/Word.thy Thu Nov 17 12:29:48 2011 +0100
+++ b/src/HOL/Word/Word.thy Thu Nov 17 12:38:03 2011 +0100
@@ -121,7 +121,7 @@
subsection "Arithmetic operations"
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
+instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord}"
begin
definition
@@ -157,22 +157,6 @@
definition
word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
-definition
- word_and_def:
- "(a::'a word) AND b = word_of_int (uint a AND uint b)"
-
-definition
- word_or_def:
- "(a::'a word) OR b = word_of_int (uint a OR uint b)"
-
-definition
- word_xor_def:
- "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
-
-definition
- word_not_def:
- "NOT (a::'a word) = word_of_int (NOT (uint a))"
-
instance ..
end
@@ -204,6 +188,22 @@
begin
definition
+ word_and_def:
+ "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+
+definition
+ word_or_def:
+ "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+
+definition
+ word_xor_def:
+ "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+
+definition
+ word_not_def:
+ "NOT (a::'a word) = word_of_int (NOT (uint a))"
+
+definition
word_test_bit_def: "test_bit a = bin_nth (uint a)"
definition