--- a/src/HOL/Library/Boolean_Algebra.thy Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Boolean_Algebra.thy Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
Author: Brian Huffman
*)
-section {* Boolean Algebras *}
+section \<open>Boolean Algebras\<close>
theory Boolean_Algebra
imports Main
@@ -53,7 +53,7 @@
apply (rule conj_cancel_right)
done
-subsection {* Complement *}
+subsection \<open>Complement\<close>
lemma complement_unique:
assumes 1: "a \<sqinter> x = \<zero>"
@@ -81,7 +81,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 {* Conjunction *}
+subsection \<open>Conjunction\<close>
lemma conj_absorb [simp]: "x \<sqinter> x = x"
proof -
@@ -124,7 +124,7 @@
lemmas conj_disj_distribs =
conj_disj_distrib conj_disj_distrib2
-subsection {* Disjunction *}
+subsection \<open>Disjunction\<close>
lemma disj_absorb [simp]: "x \<squnion> x = x"
by (rule boolean.conj_absorb [OF dual])
@@ -154,7 +154,7 @@
lemmas disj_conj_distribs =
disj_conj_distrib disj_conj_distrib2
-subsection {* De Morgan's Laws *}
+subsection \<open>De Morgan's Laws\<close>
lemma de_Morgan_conj [simp]: "\<sim> (x \<sqinter> y) = \<sim> x \<squnion> \<sim> y"
proof (rule compl_unique)
@@ -178,7 +178,7 @@
end
-subsection {* Symmetric Difference *}
+subsection \<open>Symmetric Difference\<close>
locale boolean_xor = boolean +
fixes xor :: "'a => 'a => 'a" (infixr "\<oplus>" 65)