src/HOL/Library/Boolean_Algebra.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60855 6449ae4b85f9
     1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Boolean Algebras *}
     1.8 +section \<open>Boolean Algebras\<close>
     1.9  
    1.10  theory Boolean_Algebra
    1.11  imports Main
    1.12 @@ -53,7 +53,7 @@
    1.13  apply (rule conj_cancel_right)
    1.14  done
    1.15  
    1.16 -subsection {* Complement *}
    1.17 +subsection \<open>Complement\<close>
    1.18  
    1.19  lemma complement_unique:
    1.20    assumes 1: "a \<sqinter> x = \<zero>"
    1.21 @@ -81,7 +81,7 @@
    1.22  lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
    1.23  by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
    1.24  
    1.25 -subsection {* Conjunction *}
    1.26 +subsection \<open>Conjunction\<close>
    1.27  
    1.28  lemma conj_absorb [simp]: "x \<sqinter> x = x"
    1.29  proof -
    1.30 @@ -124,7 +124,7 @@
    1.31  lemmas conj_disj_distribs =
    1.32     conj_disj_distrib conj_disj_distrib2
    1.33  
    1.34 -subsection {* Disjunction *}
    1.35 +subsection \<open>Disjunction\<close>
    1.36  
    1.37  lemma disj_absorb [simp]: "x \<squnion> x = x"
    1.38  by (rule boolean.conj_absorb [OF dual])
    1.39 @@ -154,7 +154,7 @@
    1.40  lemmas disj_conj_distribs =
    1.41     disj_conj_distrib disj_conj_distrib2
    1.42  
    1.43 -subsection {* De Morgan's Laws *}
    1.44 +subsection \<open>De Morgan's Laws\<close>
    1.45  
    1.46  lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
    1.47  proof (rule compl_unique)
    1.48 @@ -178,7 +178,7 @@
    1.49  
    1.50  end
    1.51  
    1.52 -subsection {* Symmetric Difference *}
    1.53 +subsection \<open>Symmetric Difference\<close>
    1.54  
    1.55  locale boolean_xor = boolean +
    1.56    fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)