diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -3,15 +3,15 @@
    Author:   Alexander Krauss, TU Muenchen
 *)
 
-section {* Chain-complete partial orders and their fixpoints *}
+section \<open>Chain-complete partial orders and their fixpoints\<close>
 
 theory Complete_Partial_Order
 imports Product_Type
 begin
 
-subsection {* Monotone functions *}
+subsection \<open>Monotone functions\<close>
 
-text {* Dictionary-passing version of @{const Orderings.mono}. *}
+text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close>
 
 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
 where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
@@ -24,11 +24,11 @@
 unfolding monotone_def by iprover
 
 
-subsection {* Chains *}
+subsection \<open>Chains\<close>
 
-text {* A chain is a totally-ordered set. Chains are parameterized over
+text \<open>A chain is a totally-ordered set. Chains are parameterized over
   the order for maximal flexibility, since type classes are not enough.
-*}
+\<close>
 
 definition
   chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
@@ -67,12 +67,12 @@
   shows "chain le_b (f ` Y)"
 by(blast intro: chainI dest: chainD[OF chain] mono)
 
-subsection {* Chain-complete partial orders *}
+subsection \<open>Chain-complete partial orders\<close>
 
-text {*
+text \<open>
   A ccpo has a least upper bound for any chain.  In particular, the
   empty set is a chain, so every ccpo must have a bottom element.
-*}
+\<close>
 
 class ccpo = order + Sup +
   assumes ccpo_Sup_upper: "\<lbrakk>chain (op \<le>) A; x \<in> A\<rbrakk> \<Longrightarrow> x \<le> Sup A"
@@ -85,7 +85,7 @@
 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
 by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
 
-subsection {* Transfinite iteration of a function *}
+subsection \<open>Transfinite iteration of a function\<close>
 
 inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
 for f :: "'a \<Rightarrow> 'a"
@@ -145,7 +145,7 @@
 lemma bot_in_iterates: "Sup {} \<in> iterates f"
 by(auto intro: iterates.Sup simp add: chain_empty)
 
-subsection {* Fixpoint combinator *}
+subsection \<open>Fixpoint combinator\<close>
 
 definition
   fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -183,9 +183,9 @@
 
 end
 
-subsection {* Fixpoint induction *}
+subsection \<open>Fixpoint induction\<close>
 
-setup {* Sign.map_naming (Name_Space.mandatory_path "ccpo") *}
+setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
 
 definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
@@ -203,7 +203,7 @@
   shows "P (lub A)"
 using assms by (auto simp: ccpo.admissible_def)
 
-setup {* Sign.map_naming Name_Space.parent_path *}
+setup \<open>Sign.map_naming Name_Space.parent_path\<close>
 
 lemma (in ccpo) fixp_induct:
   assumes adm: "ccpo.admissible Sup (op \<le>) P"