diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Lattices.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -2,19 +2,19 @@
     Author:     Tobias Nipkow
 *)
 
-section {* Abstract lattices *}
+section \<open>Abstract lattices\<close>
 
 theory Lattices
 imports Groups
 begin
 
-subsection {* Abstract semilattice *}
+subsection \<open>Abstract semilattice\<close>
 
-text {*
+text \<open>
   These locales provide a basic structure for interpretation into
   bigger structures;  extensions require careful thinking, otherwise
   undesired effects may occur due to interpretation.
-*}
+\<close>
 
 no_notation times (infixl "*" 70)
 no_notation Groups.one ("1")
@@ -73,7 +73,7 @@
     by simp
   then have "a = (a * b) * c"
     by (simp add: assoc)
-  with `a = a * b` [symmetric] have "a = a * c" by simp
+  with \<open>a = a * b\<close> [symmetric] have "a = a * c" by simp
   then show "a \<preceq> c" by (rule orderI)
 qed
 
@@ -153,7 +153,7 @@
 notation Groups.one ("1")
 
 
-subsection {* Syntactic infimum and supremum operations *}
+subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class inf =
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -162,7 +162,7 @@
   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
 
 
-subsection {* Concrete lattices *}
+subsection \<open>Concrete lattices\<close>
 
 notation
   less_eq  (infix "\<sqsubseteq>" 50) and
@@ -179,7 +179,7 @@
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
 begin
 
-text {* Dual lattice *}
+text \<open>Dual lattice\<close>
 
 lemma dual_semilattice:
   "class.semilattice_inf sup greater_eq greater"
@@ -191,7 +191,7 @@
 class lattice = semilattice_inf + semilattice_sup
 
 
-subsubsection {* Intro and elim rules*}
+subsubsection \<open>Intro and elim rules\<close>
 
 context semilattice_inf
 begin
@@ -266,7 +266,7 @@
 end
 
 
-subsubsection {* Equational laws *}
+subsubsection \<open>Equational laws\<close>
 
 context semilattice_inf
 begin
@@ -373,7 +373,7 @@
 
 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
 
-text{* Towards distributivity *}
+text\<open>Towards distributivity\<close>
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
@@ -381,7 +381,7 @@
 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
-text{* If you have one of them, you have them all. *}
+text\<open>If you have one of them, you have them all.\<close>
 
 lemma distrib_imp1:
 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -411,7 +411,7 @@
 
 end
 
-subsubsection {* Strict order *}
+subsubsection \<open>Strict order\<close>
 
 context semilattice_inf
 begin
@@ -442,7 +442,7 @@
 end
 
 
-subsection {* Distributive lattices *}
+subsection \<open>Distributive lattices\<close>
 
 class distrib_lattice = lattice +
   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
@@ -479,7 +479,7 @@
 end
 
 
-subsection {* Bounded lattices and boolean algebras *}
+subsection \<open>Bounded lattices and boolean algebras\<close>
 
 class bounded_semilattice_inf_top = semilattice_inf + order_top
 begin
@@ -710,7 +710,7 @@
 end
 
 
-subsection {* @{text "min/max"} as special case of lattice *}
+subsection \<open>@{text "min/max"} as special case of lattice\<close>
 
 context linorder
 begin
@@ -788,7 +788,7 @@
   by (auto intro: antisym simp add: max_def fun_eq_iff)
 
 
-subsection {* Uniqueness of inf and sup *}
+subsection \<open>Uniqueness of inf and sup\<close>
 
 lemma (in semilattice_inf) inf_unique:
   fixes f (infixl "\<triangle>" 70)
@@ -815,7 +815,7 @@
 qed
 
 
-subsection {* Lattice on @{typ bool} *}
+subsection \<open>Lattice on @{typ bool}\<close>
 
 instantiation bool :: boolean_algebra
 begin
@@ -850,7 +850,7 @@
   by auto
 
 
-subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
+subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close>
 
 instantiation "fun" :: (type, semilattice_sup) semilattice_sup
 begin
@@ -921,7 +921,7 @@
 qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
 
 
-subsection {* Lattice on unary and binary predicates *}
+subsection \<open>Lattice on unary and binary predicates\<close>
 
 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
   by (simp add: inf_fun_def)
@@ -965,10 +965,10 @@
 lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   by (simp add: sup_fun_def) iprover
 
-text {*
+text \<open>
   \medskip Classical introduction rule: no commitment to @{text A} vs
   @{text B}.
-*}
+\<close>
 
 lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   by (auto simp add: sup_fun_def)