src/HOL/Library/Boolean_Algebra.thy
changeset 54868 bab6cade3cc5
parent 34973 ae634fad947e
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Thu Dec 26 22:47:49 2013 +0100
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Fri Dec 27 14:35:14 2013 +0100
     1.3 @@ -24,16 +24,14 @@
     1.4    assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
     1.5    assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
     1.6    assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
     1.7 +begin
     1.8  
     1.9 -sublocale boolean < conj!: abel_semigroup conj proof
    1.10 +sublocale conj!: abel_semigroup conj proof
    1.11  qed (fact conj_assoc conj_commute)+
    1.12  
    1.13 -sublocale boolean < disj!: abel_semigroup disj proof
    1.14 +sublocale disj!: abel_semigroup disj proof
    1.15  qed (fact disj_assoc disj_commute)+
    1.16  
    1.17 -context boolean
    1.18 -begin
    1.19 -
    1.20  lemmas conj_left_commute = conj.left_commute
    1.21  
    1.22  lemmas disj_left_commute = disj.left_commute
    1.23 @@ -185,8 +183,9 @@
    1.24  locale boolean_xor = boolean +
    1.25    fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
    1.26    assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
    1.27 +begin
    1.28  
    1.29 -sublocale boolean_xor < xor!: abel_semigroup xor proof
    1.30 +sublocale xor!: abel_semigroup xor proof
    1.31    fix x y z :: 'a
    1.32    let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
    1.33              (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
    1.34 @@ -201,9 +200,6 @@
    1.35      by (simp only: xor_def conj_commute disj_commute)
    1.36  qed
    1.37  
    1.38 -context boolean_xor
    1.39 -begin
    1.40 -
    1.41  lemmas xor_assoc = xor.assoc
    1.42  lemmas xor_commute = xor.commute
    1.43  lemmas xor_left_commute = xor.left_commute