diff -r ac1706cdde25 -r 18e94864fd0f src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Apr 20 13:44:16 2019 +0000
+++ b/src/HOL/Word/Word.thy	Sat Apr 20 18:02:20 2019 +0000
@@ -4202,8 +4202,8 @@
 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)
@@ -4216,17 +4216,17 @@
   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