1.1 --- a/src/HOL/Word/Word.thy	Thu Nov 17 12:29:48 2011 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Nov 17 12:38:03 2011 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4  
     1.5  subsection  "Arithmetic operations"
     1.6  
     1.7 -instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
     1.8 +instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord}"
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -157,22 +157,6 @@
    1.13  definition
    1.14    word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
    1.15  
    1.16 -definition
    1.17 -  word_and_def: 
    1.18 -  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
    1.19 -
    1.20 -definition
    1.21 -  word_or_def:  
    1.22 -  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
    1.23 -
    1.24 -definition
    1.25 -  word_xor_def: 
    1.26 -  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
    1.27 -
    1.28 -definition
    1.29 -  word_not_def: 
    1.30 -  "NOT (a::'a word) = word_of_int (NOT (uint a))"
    1.31 -
    1.32  instance ..
    1.33  
    1.34  end
    1.35 @@ -204,6 +188,22 @@
    1.36  begin
    1.37  
    1.38  definition
    1.39 +  word_and_def: 
    1.40 +  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
    1.41 +
    1.42 +definition
    1.43 +  word_or_def:  
    1.44 +  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
    1.45 +
    1.46 +definition
    1.47 +  word_xor_def: 
    1.48 +  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
    1.49 +
    1.50 +definition
    1.51 +  word_not_def: 
    1.52 +  "NOT (a::'a word) = word_of_int (NOT (uint a))"
    1.53 +
    1.54 +definition
    1.55    word_test_bit_def: "test_bit a = bin_nth (uint a)"
    1.56  
    1.57  definition