diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Upper powerdomain *}
+section \<open>Upper powerdomain\<close>
 
 theory UpperPD
 imports Compact_Basis
 begin
 
-subsection {* Basis preorder *}
+subsection \<open>Basis preorder\<close>
 
 definition
   upper_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<sharp>" 50) where
@@ -70,7 +70,7 @@
 done
 
 
-subsection {* Type definition *}
+subsection \<open>Type definition\<close>
 
 typedef 'a upper_pd  ("('(_')\<sharp>)") =
   "{S::'a pd_basis set. upper_le.ideal S}"
@@ -103,7 +103,7 @@
 using upper_principal_def pd_basis_countable
 by (rule upper_le.typedef_ideal_completion)
 
-text {* Upper powerdomain is pointed *}
+text \<open>Upper powerdomain is pointed\<close>
 
 lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: upper_pd.principal_induct, simp, simp)
@@ -115,7 +115,7 @@
 by (rule upper_pd_minimal [THEN bottomI, symmetric])
 
 
-subsection {* Monadic unit and plus *}
+subsection \<open>Monadic unit and plus\<close>
 
 definition
   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
@@ -174,11 +174,11 @@
 lemmas upper_plus_left_commute = upper_add.left_commute
 lemmas upper_plus_left_absorb = upper_add.left_idem
 
-text {* Useful for @{text "simp add: upper_plus_ac"} *}
+text \<open>Useful for \<open>simp add: upper_plus_ac\<close>\<close>
 lemmas upper_plus_ac =
   upper_plus_assoc upper_plus_commute upper_plus_left_commute
 
-text {* Useful for @{text "simp only: upper_plus_aci"} *}
+text \<open>Useful for \<open>simp only: upper_plus_aci\<close>\<close>
 lemmas upper_plus_aci =
   upper_plus_ac upper_plus_absorb upper_plus_left_absorb
 
@@ -261,7 +261,7 @@
 by (auto dest!: upper_pd.compact_imp_principal)
 
 
-subsection {* Induction rules *}
+subsection \<open>Induction rules\<close>
 
 lemma upper_pd_induct1:
   assumes P: "adm P"
@@ -290,7 +290,7 @@
 done
 
 
-subsection {* Monadic bind *}
+subsection \<open>Monadic bind\<close>
 
 definition
   upper_bind_basis ::
@@ -362,7 +362,7 @@
 by (induct xs, simp_all)
 
 
-subsection {* Map *}
+subsection \<open>Map\<close>
 
 definition
   upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
@@ -453,7 +453,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Upper powerdomain is bifinite *}
+subsection \<open>Upper powerdomain is bifinite\<close>
 
 lemma approx_chain_upper_map:
   assumes "approx_chain a"
@@ -468,7 +468,7 @@
     by (fast intro!: approx_chain_upper_map)
 qed
 
-subsection {* Join *}
+subsection \<open>Join\<close>
 
 definition
   upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where