src/HOL/Library/Boolean_Algebra.thy
changeset 54868 bab6cade3cc5
parent 34973 ae634fad947e
child 58881 b9556a055632
--- a/src/HOL/Library/Boolean_Algebra.thy	Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Fri Dec 27 14:35:14 2013 +0100
@@ -24,16 +24,14 @@
   assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
   assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
   assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
+begin
 
-sublocale boolean < conj!: abel_semigroup conj proof
+sublocale conj!: abel_semigroup conj proof
 qed (fact conj_assoc conj_commute)+
 
-sublocale boolean < disj!: abel_semigroup disj proof
+sublocale disj!: abel_semigroup disj proof
 qed (fact disj_assoc disj_commute)+
 
-context boolean
-begin
-
 lemmas conj_left_commute = conj.left_commute
 
 lemmas disj_left_commute = disj.left_commute
@@ -185,8 +183,9 @@
 locale boolean_xor = boolean +
   fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
   assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
+begin
 
-sublocale boolean_xor < 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)"
@@ -201,9 +200,6 @@
     by (simp only: xor_def conj_commute disj_commute)
 qed
 
-context boolean_xor
-begin
-
 lemmas xor_assoc = xor.assoc
 lemmas xor_commute = xor.commute
 lemmas xor_left_commute = xor.left_commute