diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Up.thy
--- a/src/HOL/HOLCF/Up.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Up.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The type of lifted values *}
+section \<open>The type of lifted values\<close>
 
 theory Up
 imports Cfun
@@ -11,7 +11,7 @@
 
 default_sort cpo
 
-subsection {* Definition of new type for lifting *}
+subsection \<open>Definition of new type for lifting\<close>
 
 datatype 'a u  ("(_\<^sub>\<bottom>)" [1000] 999) = Ibottom | Iup 'a
 
@@ -19,7 +19,7 @@
     "Ifup f Ibottom = \<bottom>"
  |  "Ifup f (Iup x) = f\<cdot>x"
 
-subsection {* Ordering on lifted cpo *}
+subsection \<open>Ordering on lifted cpo\<close>
 
 instantiation u :: (cpo) below
 begin
@@ -41,7 +41,7 @@
 lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
 by (simp add: below_up_def)
 
-subsection {* Lifted cpo is a partial order *}
+subsection \<open>Lifted cpo is a partial order\<close>
 
 instance u :: (cpo) po
 proof
@@ -60,7 +60,7 @@
     by (auto split: u.split_asm intro: below_trans)
 qed
 
-subsection {* Lifted cpo is a cpo *}
+subsection \<open>Lifted cpo is a cpo\<close>
 
 lemma is_lub_Iup:
   "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
@@ -117,18 +117,18 @@
   qed
 qed
 
-subsection {* Lifted cpo is pointed *}
+subsection \<open>Lifted cpo is pointed\<close>
 
 instance u :: (cpo) pcpo
 by intro_classes fast
 
-text {* for compatibility with old HOLCF-Version *}
+text \<open>for compatibility with old HOLCF-Version\<close>
 lemma inst_up_pcpo: "\<bottom> = Ibottom"
 by (rule minimal_up [THEN bottomI, symmetric])
 
-subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
+subsection \<open>Continuity of \emph{Iup} and \emph{Ifup}\<close>
 
-text {* continuity for @{term Iup} *}
+text \<open>continuity for @{term Iup}\<close>
 
 lemma cont_Iup: "cont Iup"
 apply (rule contI)
@@ -136,7 +136,7 @@
 apply (erule cpo_lubI)
 done
 
-text {* continuity for @{term Ifup} *}
+text \<open>continuity for @{term Ifup}\<close>
 
 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)"
 by (induct x, simp_all)
@@ -166,7 +166,7 @@
   qed simp
 qed (rule monofun_Ifup2)
 
-subsection {* Continuous versions of constants *}
+subsection \<open>Continuous versions of constants\<close>
 
 definition
   up  :: "'a \<rightarrow> 'a u" where
@@ -181,7 +181,7 @@
   "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
-text {* continuous versions of lemmas for @{typ "('a)u"} *}
+text \<open>continuous versions of lemmas for @{typ "('a)u"}\<close>
 
 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)"
 apply (induct z)
@@ -215,7 +215,7 @@
   "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
-text {* lifting preserves chain-finiteness *}
+text \<open>lifting preserves chain-finiteness\<close>
 
 lemma up_chain_cases:
   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
@@ -247,7 +247,7 @@
 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
 done
 
-text {* properties of fup *}
+text \<open>properties of fup\<close>
 
 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)