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)
```