src/HOL/Word/Word.thy

   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
 lemma word_or_not [simp]: "x OR NOT x = max_word"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-lemma word_boolean: "boolean (AND) (OR) bitNOT 0 max_word"
-  apply (rule boolean.intro)
+lemma word_boolean_algebra: "boolean_algebra (AND) (OR) bitNOT 0 max_word"
+  apply (rule boolean_algebra.intro)
            apply (rule word_bw_assocs)
           apply (rule word_bw_assocs)
          apply (rule word_bw_comms)
         apply (rule word_bw_comms)
        apply (rule word_ao_dist2)

     apply (rule word_log_esimps)
    apply (rule word_and_not)
   apply (rule word_or_not)
   done
 
-interpretation word_bool_alg: boolean "(AND)" "(OR)" bitNOT 0 max_word
-  by (rule word_boolean)
+interpretation word_bool_alg: boolean_algebra "(AND)" "(OR)" bitNOT 0 max_word
+  by (rule word_boolean_algebra)
 
 lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
   for x y :: "'a::len0 word"
   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
 
-interpretation word_bool_alg: boolean_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
-  apply (rule boolean_xor.intro)
-   apply (rule word_boolean)
-  apply (rule boolean_xor_axioms.intro)
+interpretation word_bool_alg: boolean_algebra_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
+  apply (rule boolean_algebra_xor.intro)
+   apply (rule word_boolean_algebra)
+  apply (rule boolean_algebra_xor_axioms.intro)
   apply (rule word_xor_and_or)
   done
 
 lemma shiftr_x_0 [iff]: "x >> 0 = x"
   for x :: "'a::len0 word"