# HG changeset patch
# User wenzelm
# Date 1438864145 -7200
# Node ID 6449ae4b85f9d844c5c75cfb85877a14da38fd30
# Parent  8f45dd297357be8bb1ed4ca8c9aa1d5959202c6f
tuned;

diff -r 8f45dd297357 -r 6449ae4b85f9 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:28:59 2015 +0200
+++ b/src/HOL/Library/Boolean_Algebra.thy	Thu Aug 06 14:29:05 2015 +0200
@@ -26,11 +26,11 @@
   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
 begin
 
-sublocale conj!: abel_semigroup conj proof
-qed (fact conj_assoc conj_commute)+
+sublocale conj!: abel_semigroup conj
+  by standard (fact conj_assoc conj_commute)+
 
-sublocale disj!: abel_semigroup disj proof
-qed (fact disj_assoc disj_commute)+
+sublocale disj!: abel_semigroup disj
+  by standard (fact disj_assoc disj_commute)+
 
 lemmas conj_left_commute = conj.left_commute
 
@@ -53,6 +53,7 @@
 apply (rule conj_cancel_right)
 done
 
+
 subsection \<open>Complement\<close>
 
 lemma complement_unique:
@@ -81,6 +82,7 @@
 lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
 by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
 
+
 subsection \<open>Conjunction\<close>
 
 lemma conj_absorb [simp]: "x \<sqinter> x = x"
@@ -118,12 +120,13 @@
 by (simp only: conj_assoc [symmetric] conj_absorb)
 
 lemma conj_disj_distrib2:
-  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" 
+  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
 by (simp only: conj_commute conj_disj_distrib)
 
 lemmas conj_disj_distribs =
    conj_disj_distrib conj_disj_distrib2
 
+
 subsection \<open>Disjunction\<close>
 
 lemma disj_absorb [simp]: "x \<squnion> x = x"
@@ -154,6 +157,7 @@
 lemmas disj_conj_distribs =
    disj_conj_distrib disj_conj_distrib2
 
+
 subsection \<open>De Morgan's Laws\<close>
 
 lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
@@ -178,14 +182,16 @@
 
 end
 
+
 subsection \<open>Symmetric Difference\<close>
 
 locale boolean_xor = boolean +
-  fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
+  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
 
-sublocale xor!: abel_semigroup xor proof
+sublocale xor!: abel_semigroup xor
+proof
   fix x y z :: 'a
   let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
             (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
@@ -262,8 +268,7 @@
         conj_disj_distribs conj_ac disj_ac)
 qed
 
-lemma conj_xor_distrib2:
-  "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
+lemma conj_xor_distrib2: "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
 proof -
   have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
     by (rule conj_xor_distrib)
@@ -271,8 +276,7 @@
     by (simp only: conj_commute)
 qed
 
-lemmas conj_xor_distribs =
-   conj_xor_distrib conj_xor_distrib2
+lemmas conj_xor_distribs = conj_xor_distrib conj_xor_distrib2
 
 end