# HG changeset patch
# User haftmann
# Date 1555783340 0
# Node ID 18e94864fd0f22bdb9bef5a8c017a43522489853
# Parent  ac1706cdde25403d06c61b87dae96e6b6fdf2d94
tuned name

diff -r ac1706cdde25 -r 18e94864fd0f src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 20 13:44:16 2019 +0000
+++ b/src/HOL/Library/Boolean_Algebra.thy	Sat Apr 20 18:02:20 2019 +0000
@@ -8,7 +8,7 @@
   imports Main
 begin
 
-locale boolean =
+locale boolean_algebra =
   fixes conj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<sqinter>" 70)
     and disj :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<squnion>" 65)
     and compl :: "'a \<Rightarrow> 'a"  ("\<sim> _" [81] 80)
@@ -38,8 +38,8 @@
 lemmas conj_ac = conj.assoc conj.commute conj.left_commute
 lemmas disj_ac = disj.assoc disj.commute disj.left_commute
 
-lemma dual: "boolean disj conj compl one zero"
-  apply (rule boolean.intro)
+lemma dual: "boolean_algebra disj conj compl one zero"
+  apply (rule boolean_algebra.intro)
            apply (rule disj_assoc)
           apply (rule conj_assoc)
          apply (rule disj_commute)
@@ -143,28 +143,28 @@
 subsection \<open>Disjunction\<close>
 
 lemma disj_absorb [simp]: "x \<squnion> x = x"
-  by (rule boolean.conj_absorb [OF dual])
+  by (rule boolean_algebra.conj_absorb [OF dual])
 
 lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>"
-  by (rule boolean.conj_zero_right [OF dual])
+  by (rule boolean_algebra.conj_zero_right [OF dual])
 
 lemma compl_zero [simp]: "\<sim> \<zero> = \<one>"
-  by (rule boolean.compl_one [OF dual])
+  by (rule boolean_algebra.compl_one [OF dual])
 
 lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x"
-  by (rule boolean.conj_one_left [OF dual])
+  by (rule boolean_algebra.conj_one_left [OF dual])
 
 lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>"
-  by (rule boolean.conj_zero_left [OF dual])
+  by (rule boolean_algebra.conj_zero_left [OF dual])
 
 lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>"
-  by (rule boolean.conj_cancel_left [OF dual])
+  by (rule boolean_algebra.conj_cancel_left [OF dual])
 
 lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-  by (rule boolean.conj_left_absorb [OF dual])
+  by (rule boolean_algebra.conj_left_absorb [OF dual])
 
 lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-  by (rule boolean.conj_disj_distrib2 [OF dual])
+  by (rule boolean_algebra.conj_disj_distrib2 [OF dual])
 
 lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2
 
@@ -189,14 +189,14 @@
 qed
 
 lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
-  by (rule boolean.de_Morgan_conj [OF dual])
+  by (rule boolean_algebra.de_Morgan_conj [OF dual])
 
 end
 
 
 subsection \<open>Symmetric Difference\<close>
 
-locale boolean_xor = boolean +
+locale boolean_algebra_xor = boolean_algebra +
   fixes xor :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "\<oplus>" 65)
   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
 begin
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