# HG changeset patch
# User wenzelm
# Date 1452722826 -3600
# Node ID 8ffc4d0e652dd3c40fd474eacf725493b2fdd0a2
# Parent  fae6233c5f37ca25ef5317e92b7b8a473d8721d4
isabelle update_cartouches -c -t;

diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Adm.thy
--- a/src/HOL/HOLCF/Adm.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Adm.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger and Brian Huffman
 *)
 
-section {* Admissibility and compactness *}
+section \<open>Admissibility and compactness\<close>
 
 theory Adm
 imports Cont
@@ -10,7 +10,7 @@
 
 default_sort cpo
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 definition
   adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool" where
@@ -29,14 +29,14 @@
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)
 
-subsection {* Admissibility on chain-finite types *}
+subsection \<open>Admissibility on chain-finite types\<close>
 
-text {* For chain-finite (easy) types every formula is admissible. *}
+text \<open>For chain-finite (easy) types every formula is admissible.\<close>
 
 lemma adm_chfin [simp]: "adm (P::'a::chfin \<Rightarrow> bool)"
 by (rule admI, frule chfin, auto simp add: maxinch_is_thelub)
 
-subsection {* Admissibility of special formulae and propagation *}
+subsection \<open>Admissibility of special formulae and propagation\<close>
 
 lemma adm_const [simp]: "adm (\<lambda>x. t)"
 by (rule admI, simp)
@@ -53,7 +53,7 @@
   "(\<And>y. y \<in> A \<Longrightarrow> adm (\<lambda>x. P x y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y\<in>A. P x y)"
 by (fast intro: admI elim: admD)
 
-text {* Admissibility for disjunction is hard to prove. It requires 2 lemmas. *}
+text \<open>Admissibility for disjunction is hard to prove. It requires 2 lemmas.\<close>
 
 lemma adm_disj_lemma1:
   assumes adm: "adm P"
@@ -108,7 +108,7 @@
     \<Longrightarrow> adm (\<lambda>x. P x = Q x)"
 by (subst iff_conv_conj_imp, rule adm_conj)
 
-text {* admissibility and continuity *}
+text \<open>admissibility and continuity\<close>
 
 lemma adm_below [simp]:
   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
@@ -124,7 +124,7 @@
 lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
 by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
 
-subsection {* Compactness *}
+subsection \<open>Compactness\<close>
 
 definition
   compact :: "'a::cpo \<Rightarrow> bool" where
@@ -161,7 +161,7 @@
 apply (erule (1) below_trans [OF is_ub_thelub])
 done
 
-text {* admissibility and compactness *}
+text \<open>admissibility and compactness\<close>
 
 lemma adm_compact_not_below [simp]:
   "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
@@ -178,7 +178,7 @@
 lemma compact_bottom [simp, intro]: "compact \<bottom>"
 by (rule compactI, simp)
 
-text {* Any upward-closed predicate is admissible. *}
+text \<open>Any upward-closed predicate is admissible.\<close>
 
 lemma adm_upward:
   assumes P: "\<And>x y. \<lbrakk>P x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> P y"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Algebraic.thy
--- a/src/HOL/HOLCF/Algebraic.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Algebraic.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Algebraic deflations *}
+section \<open>Algebraic deflations\<close>
 
 theory Algebraic
 imports Universal Map_Functions
@@ -10,7 +10,7 @@
 
 default_sort bifinite
 
-subsection {* Type constructor for finite deflations *}
+subsection \<open>Type constructor for finite deflations\<close>
 
 typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
 by (fast intro: finite_deflation_bottom)
@@ -72,7 +72,7 @@
 using finite_deflation_Rep_fin_defl
 by (rule finite_deflation_imp_compact)
 
-subsection {* Defining algebraic deflations by ideal completion *}
+subsection \<open>Defining algebraic deflations by ideal completion\<close>
 
 typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
 by (rule below.ex_ideal)
@@ -132,7 +132,7 @@
 using defl_principal_def fin_defl_countable
 by (rule below.typedef_ideal_completion)
 
-text {* Algebraic deflations are pointed *}
+text \<open>Algebraic deflations are pointed\<close>
 
 lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
 apply (induct x rule: defl.principal_induct, simp)
@@ -147,7 +147,7 @@
 lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
 by (rule defl_minimal [THEN bottomI, symmetric])
 
-subsection {* Applying algebraic deflations *}
+subsection \<open>Applying algebraic deflations\<close>
 
 definition
   cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
@@ -215,7 +215,7 @@
 lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
 by (rule cast.below [THEN bottomI])
 
-subsection {* Deflation combinators *}
+subsection \<open>Deflation combinators\<close>
 
 definition
   "defl_fun1 e p f =
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Bifinite.thy
--- a/src/HOL/HOLCF/Bifinite.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Profinite and bifinite cpos *}
+section \<open>Profinite and bifinite cpos\<close>
 
 theory Bifinite
 imports Map_Functions "~~/src/HOL/Library/Countable"
@@ -10,7 +10,7 @@
 
 default_sort cpo
 
-subsection {* Chains of finite deflations *}
+subsection \<open>Chains of finite deflations\<close>
 
 locale approx_chain =
   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
@@ -43,7 +43,7 @@
 
 end
 
-subsection {* Omega-profinite and bifinite domains *}
+subsection \<open>Omega-profinite and bifinite domains\<close>
 
 class bifinite = pcpo +
   assumes bifinite: "\<exists>(a::nat \<Rightarrow> 'a \<rightarrow> 'a). approx_chain a"
@@ -51,7 +51,7 @@
 class profinite = cpo +
   assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
 
-subsection {* Building approx chains *}
+subsection \<open>Building approx chains\<close>
 
 lemma approx_chain_iso:
   assumes a: "approx_chain a"
@@ -102,7 +102,7 @@
   using assms unfolding approx_chain_def
   by (simp add: lub_APP prod_map_ID finite_deflation_prod_map)
 
-text {* Approx chains for countable discrete types. *}
+text \<open>Approx chains for countable discrete types.\<close>
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
@@ -152,7 +152,7 @@
 using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
 by (rule approx_chain.intro)
 
-subsection {* Class instance proofs *}
+subsection \<open>Class instance proofs\<close>
 
 instance bifinite \<subseteq> profinite
 proof
@@ -164,9 +164,9 @@
 instance u :: (profinite) bifinite
   by standard (rule profinite)
 
-text {*
+text \<open>
   Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
-*}
+\<close>
 
 definition "encode_cfun = (\<Lambda> f. sfun_abs\<cdot>(fup\<cdot>f))"
 
@@ -194,9 +194,9 @@
     by - (rule exI)
 qed
 
-text {*
+text \<open>
   Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
-*}
+\<close>
 
 definition "encode_prod_u = (\<Lambda>(up\<cdot>(x, y)). (:up\<cdot>x, up\<cdot>y:))"
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The type of continuous functions *}
+section \<open>The type of continuous functions\<close>
 
 theory Cfun
 imports Cpodef Fun_Cpo Product_Cpo
@@ -11,7 +11,7 @@
 
 default_sort cpo
 
-subsection {* Definition of continuous function type *}
+subsection \<open>Definition of continuous function type\<close>
 
 definition "cfun = {f::'a => 'b. cont f}"
 
@@ -28,22 +28,22 @@
   Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 
-subsection {* Syntax for continuous lambda abstraction *}
+subsection \<open>Syntax for continuous lambda abstraction\<close>
 
 syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
 
-parse_translation {*
+parse_translation \<open>
 (* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
   [Syntax_Trans.mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
-*}
+\<close>
 
-print_translation {*
+print_translation \<open>
   [(@{const_syntax Abs_cfun}, fn _ => fn [Abs abs] =>
       let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
       in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
-*}  -- {* To avoid eta-contraction of body *}
+\<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 
-text {* Syntax for nested abstractions *}
+text \<open>Syntax for nested abstractions\<close>
 
 syntax (ASCII)
   "_Lambda" :: "[cargs, logic] \<Rightarrow> logic"  ("(3LAM _./ _)" [1000, 10] 10)
@@ -51,7 +51,7 @@
 syntax
   "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
 
-parse_ast_translation {*
+parse_ast_translation \<open>
 (* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
 (* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
   let
@@ -60,9 +60,9 @@
             (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
       | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
   in [(@{syntax_const "_Lambda"}, K Lambda_ast_tr)] end;
-*}
+\<close>
 
-print_ast_translation {*
+print_ast_translation \<open>
 (* rewrite (_cabs x (_cabs y (_cabs z t))) => (LAM x y z. t) *)
 (* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
   let
@@ -74,13 +74,13 @@
           [Ast.Constant @{syntax_const "_Lambda"},
            Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
   in [(@{syntax_const "_cabs"}, K cabs_ast_tr')] end
-*}
+\<close>
 
-text {* Dummy patterns for continuous abstraction *}
+text \<open>Dummy patterns for continuous abstraction\<close>
 translations
   "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
 
-subsection {* Continuous function space is pointed *}
+subsection \<open>Continuous function space is pointed\<close>
 
 lemma bottom_cfun: "\<bottom> \<in> cfun"
 by (simp add: cfun_def inst_fun_pcpo)
@@ -97,7 +97,7 @@
 lemmas Abs_cfun_strict =
   typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
 
-text {* function application is strict in its first argument *}
+text \<open>function application is strict in its first argument\<close>
 
 lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
 by (simp add: Rep_cfun_strict)
@@ -105,13 +105,13 @@
 lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
 by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
 
-text {* for compatibility with old HOLCF-Version *}
+text \<open>for compatibility with old HOLCF-Version\<close>
 lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
 by simp
 
-subsection {* Basic properties of continuous functions *}
+subsection \<open>Basic properties of continuous functions\<close>
 
-text {* Beta-equality for continuous functions *}
+text \<open>Beta-equality for continuous functions\<close>
 
 lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
 by (simp add: Abs_cfun_inverse cfun_def)
@@ -119,25 +119,25 @@
 lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
 by (simp add: Abs_cfun_inverse2)
 
-text {* Beta-reduction simproc *}
+text \<open>Beta-reduction simproc\<close>
 
-text {*
+text \<open>
   Given the term @{term "(\<Lambda> x. f x)\<cdot>y"}, the procedure tries to
   construct the theorem @{term "(\<Lambda> x. f x)\<cdot>y == f y"}.  If this
   theorem cannot be completely solved by the cont2cont rules, then
-  the procedure returns the ordinary conditional @{text beta_cfun}
+  the procedure returns the ordinary conditional \<open>beta_cfun\<close>
   rule.
 
   The simproc does not solve any more goals that would be solved by
-  using @{text beta_cfun} as a simp rule.  The advantage of the
+  using \<open>beta_cfun\<close> as a simp rule.  The advantage of the
   simproc is that it can avoid deeply-nested calls to the simplifier
   that would otherwise be caused by large continuity side conditions.
 
-  Update: The simproc now uses rule @{text Abs_cfun_inverse2} instead
-  of @{text beta_cfun}, to avoid problems with eta-contraction.
-*}
+  Update: The simproc now uses rule \<open>Abs_cfun_inverse2\<close> instead
+  of \<open>beta_cfun\<close>, to avoid problems with eta-contraction.
+\<close>
 
-simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {*
+simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = \<open>
   fn phi => fn ctxt => fn ct =>
     let
       val dest = Thm.dest_comb;
@@ -148,14 +148,14 @@
       val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
       val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
     in SOME (perhaps (SINGLE (tac 1)) tr) end
-*}
+\<close>
 
-text {* Eta-equality for continuous functions *}
+text \<open>Eta-equality for continuous functions\<close>
 
 lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
 by (rule Rep_cfun_inverse)
 
-text {* Extensionality for continuous functions *}
+text \<open>Extensionality for continuous functions\<close>
 
 lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
 by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
@@ -163,7 +163,7 @@
 lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
 by (simp add: cfun_eq_iff)
 
-text {* Extensionality wrt. ordering for continuous functions *}
+text \<open>Extensionality wrt. ordering for continuous functions\<close>
 
 lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
 by (simp add: below_cfun_def fun_below_iff)
@@ -171,7 +171,7 @@
 lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
 by (simp add: cfun_below_iff)
 
-text {* Congruence for continuous function application *}
+text \<open>Congruence for continuous function application\<close>
 
 lemma cfun_cong: "\<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f\<cdot>x = g\<cdot>y"
 by simp
@@ -182,7 +182,7 @@
 lemma cfun_arg_cong: "x = y \<Longrightarrow> f\<cdot>x = f\<cdot>y"
 by simp
 
-subsection {* Continuity of application *}
+subsection \<open>Continuity of application\<close>
 
 lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
 by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
@@ -197,7 +197,7 @@
 lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono]
 lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono]
 
-text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
+text \<open>contlub, cont properties of @{term Rep_cfun} in each argument\<close>
 
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
 by (rule cont_Rep_cfun2 [THEN cont2contlubE])
@@ -205,7 +205,7 @@
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
 by (rule cont_Rep_cfun1 [THEN cont2contlubE])
 
-text {* monotonicity of application *}
+text \<open>monotonicity of application\<close>
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
 by (simp add: cfun_below_iff)
@@ -216,7 +216,7 @@
 lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
 by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
 
-text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
+text \<open>ch2ch - rules for the type @{typ "'a -> 'b"}\<close>
 
 lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
 by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
@@ -235,7 +235,7 @@
   "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
 by (simp add: chain_def cfun_below_iff)
 
-text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
+text \<open>contlub, cont properties of @{term Rep_cfun} in both arguments\<close>
 
 lemma lub_APP:
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
@@ -248,7 +248,7 @@
 
 lemmas lub_distribs = lub_APP lub_LAM
 
-text {* strictness *}
+text \<open>strictness\<close>
 
 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
 apply (rule bottomI)
@@ -256,14 +256,14 @@
 apply (rule minimal [THEN monofun_cfun_arg])
 done
 
-text {* type @{typ "'a -> 'b"} is chain complete *}
+text \<open>type @{typ "'a -> 'b"} is chain complete\<close>
 
 lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
 by (simp add: lub_cfun lub_fun ch2ch_lambda)
 
-subsection {* Continuity simplification procedure *}
+subsection \<open>Continuity simplification procedure\<close>
 
-text {* cont2cont lemma for @{term Rep_cfun} *}
+text \<open>cont2cont lemma for @{term Rep_cfun}\<close>
 
 lemma cont2cont_APP [simp, cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
@@ -276,10 +276,10 @@
     using t cont_Rep_cfun2 1 by (rule cont_apply)
 qed
 
-text {*
+text \<open>
   Two specific lemmas for the combination of LCF and HOL terms.
   These lemmas are needed in theories that use types like @{typ "'a \<rightarrow> 'b \<Rightarrow> 'c"}.
-*}
+\<close>
 
 lemma cont_APP_app [simp]: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. ((f x)\<cdot>(g x)) s)"
 by (rule cont2cont_APP [THEN cont2cont_fun])
@@ -288,19 +288,19 @@
 by (rule cont_APP_app [THEN cont2cont_fun])
 
 
-text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
+text \<open>cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"}\<close>
 
 lemma cont2mono_LAM:
   "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
     \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
   unfolding monofun_def cfun_below_iff by simp
 
-text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
+text \<open>cont2cont Lemma for @{term "%x. LAM y. f x y"}\<close>
 
-text {*
+text \<open>
   Not suitable as a cont2cont rule, because on nested lambdas
   it causes exponential blow-up in the number of subgoals.
-*}
+\<close>
 
 lemma cont2cont_LAM:
   assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
@@ -312,10 +312,10 @@
   from f2 show "cont f" by (rule cont2cont_lambda)
 qed
 
-text {*
+text \<open>
   This version does work as a cont2cont rule, since it
   has only a single subgoal.
-*}
+\<close>
 
 lemma cont2cont_LAM' [simp, cont2cont]:
   fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
@@ -327,15 +327,15 @@
   "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
 by (simp add: cont2cont_LAM)
 
-subsection {* Miscellaneous *}
+subsection \<open>Miscellaneous\<close>
 
-text {* Monotonicity of @{term Abs_cfun} *}
+text \<open>Monotonicity of @{term Abs_cfun}\<close>
 
 lemma monofun_LAM:
   "\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
 by (simp add: cfun_below_iff)
 
-text {* some lemmata for functions with flat/chfin domain/range types *}
+text \<open>some lemmata for functions with flat/chfin domain/range types\<close>
 
 lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
       ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
@@ -348,9 +348,9 @@
 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
 by (rule adm_subst, simp, rule adm_chfin)
 
-subsection {* Continuous injection-retraction pairs *}
+subsection \<open>Continuous injection-retraction pairs\<close>
 
-text {* Continuous retractions are strict. *}
+text \<open>Continuous retractions are strict.\<close>
 
 lemma retraction_strict:
   "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
@@ -387,7 +387,7 @@
   "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; z \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
 by (erule contrapos_nn, rule injection_defined_rev)
 
-text {* a result about functions with flat codomain *}
+text \<open>a result about functions with flat codomain\<close>
 
 lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
 by (drule ax_flat, simp)
@@ -405,7 +405,7 @@
 apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
 done
 
-subsection {* Identity and composition *}
+subsection \<open>Identity and composition\<close>
 
 definition
   ID :: "'a \<rightarrow> 'a" where
@@ -434,13 +434,13 @@
 lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
 by (simp add: cfun_eq_iff)
 
-text {*
-  Show that interpretation of (pcpo,@{text "_->_"}) is a category.
+text \<open>
+  Show that interpretation of (pcpo,\<open>_->_\<close>) is a category.
   The class of objects is interpretation of syntactical class pcpo.
   The class of arrows  between objects @{typ 'a} and @{typ 'b} is interpret. of @{typ "'a -> 'b"}.
   The identity arrow is interpretation of @{term ID}.
-  The composition of f and g is interpretation of @{text "oo"}.
-*}
+  The composition of f and g is interpretation of \<open>oo\<close>.
+\<close>
 
 lemma ID2 [simp]: "f oo ID = f"
 by (rule cfun_eqI, simp)
@@ -451,7 +451,7 @@
 lemma assoc_oo: "f oo (g oo h) = (f oo g) oo h"
 by (rule cfun_eqI, simp)
 
-subsection {* Strictified functions *}
+subsection \<open>Strictified functions\<close>
 
 default_sort pcpo
 
@@ -492,7 +492,7 @@
 lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
 by (simp add: strictify_conv_if)
 
-subsection {* Continuity of let-bindings *}
+subsection \<open>Continuity of let-bindings\<close>
 
 lemma cont2cont_Let:
   assumes f: "cont (\<lambda>x. f x)"
@@ -514,8 +514,8 @@
     using g by (simp add: prod_cont_iff)
 qed
 
-text {* The simple version (suggested by Joachim Breitner) is needed if
-  the type of the defined term is not a cpo. *}
+text \<open>The simple version (suggested by Joachim Breitner) is needed if
+  the type of the defined term is not a cpo.\<close>
 
 lemma cont2cont_Let_simple [simp, cont2cont]:
   assumes "\<And>y. cont (\<lambda>x. g x y)"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Compact_Basis.thy
--- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* A compact basis for powerdomains *}
+section \<open>A compact basis for powerdomains\<close>
 
 theory Compact_Basis
 imports Universal
@@ -10,7 +10,7 @@
 
 default_sort bifinite
 
-subsection {* A compact basis for powerdomains *}
+subsection \<open>A compact basis for powerdomains\<close>
 
 definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
 
@@ -26,7 +26,7 @@
 lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
 by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
 
-text {* The powerdomain basis type is countable. *}
+text \<open>The powerdomain basis type is countable.\<close>
 
 lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
 proof -
@@ -40,7 +40,7 @@
   (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
 qed
 
-subsection {* Unit and plus constructors *}
+subsection \<open>Unit and plus constructors\<close>
 
 definition
   PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
@@ -91,7 +91,7 @@
 apply (rule PDUnit, erule PDPlus [OF PDUnit])
 done
 
-subsection {* Fold operator *}
+subsection \<open>Fold operator\<close>
 
 definition
   fold_pd ::
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Defining algebraic domains by ideal completion *}
+section \<open>Defining algebraic domains by ideal completion\<close>
 
 theory Completion
 imports Plain_HOLCF
 begin
 
-subsection {* Ideals over a preorder *}
+subsection \<open>Ideals over a preorder\<close>
 
 locale preorder =
   fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
@@ -52,7 +52,7 @@
 lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
 by (fast intro: ideal_principal)
 
-text {* The set of ideals is a cpo *}
+text \<open>The set of ideals is a cpo\<close>
 
 lemma ideal_UN:
   fixes A :: "nat \<Rightarrow> 'a set"
@@ -126,7 +126,7 @@
 apply (erule (1) below_trans)
 done
 
-subsection {* Lemmas about least upper bounds *}
+subsection \<open>Lemmas about least upper bounds\<close>
 
 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
 apply (erule exE, drule is_lub_lub)
@@ -137,7 +137,7 @@
 lemma is_lub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
 by (erule exE, drule is_lub_lub, erule is_lubD2)
 
-subsection {* Locale for ideal completion *}
+subsection \<open>Locale for ideal completion\<close>
 
 locale ideal_completion = preorder +
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
@@ -179,12 +179,12 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
-subsubsection {* Principal ideals approximate all elements *}
+subsubsection \<open>Principal ideals approximate all elements\<close>
 
 lemma compact_principal [simp]: "compact (principal a)"
 by (rule compactI2, simp add: principal_below_iff_mem_rep rep_lub)
 
-text {* Construct a chain whose lub is the same as a given ideal *}
+text \<open>Construct a chain whose lub is the same as a given ideal\<close>
 
 lemma obtain_principal_chain:
   obtains Y where "\<forall>i. Y i \<preceq> Y (Suc i)" and "x = (\<Squnion>i. principal (Y i))"
@@ -278,7 +278,7 @@
 apply (drule (2) admD2, fast, simp)
 done
 
-subsection {* Defining functions in terms of basis elements *}
+subsection \<open>Defining functions in terms of basis elements\<close>
 
 definition
   extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Cont.thy
--- a/src/HOL/HOLCF/Cont.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Cont.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,23 +3,23 @@
     Author:     Brian Huffman
 *)
 
-section {* Continuity and monotonicity *}
+section \<open>Continuity and monotonicity\<close>
 
 theory Cont
 imports Pcpo
 begin
 
-text {*
+text \<open>
    Now we change the default class! Form now on all untyped type variables are
    of default class po
-*}
+\<close>
 
 default_sort po
 
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
 
 definition
-  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
+  monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  \<comment> "monotonicity"  where
   "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
 definition
@@ -44,9 +44,9 @@
 by (simp add: monofun_def)
 
 
-subsection {* Equivalence of alternate definition *}
+subsection \<open>Equivalence of alternate definition\<close>
 
-text {* monotone functions map chains to chains *}
+text \<open>monotone functions map chains to chains\<close>
 
 lemma ch2ch_monofun: "\<lbrakk>monofun f; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. f (Y i))"
 apply (rule chainI)
@@ -54,7 +54,7 @@
 apply (erule chainE)
 done
 
-text {* monotone functions map upper bound to upper bounds *}
+text \<open>monotone functions map upper bound to upper bounds\<close>
 
 lemma ub2ub_monofun: 
   "\<lbrakk>monofun f; range Y <| u\<rbrakk> \<Longrightarrow> range (\<lambda>i. f (Y i)) <| f u"
@@ -63,7 +63,7 @@
 apply (erule ub_rangeD)
 done
 
-text {* a lemma about binary chains *}
+text \<open>a lemma about binary chains\<close>
 
 lemma binchain_cont:
   "\<lbrakk>cont f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> range (\<lambda>i::nat. f (if i = 0 then x else y)) <<| f y"
@@ -75,7 +75,7 @@
 apply (erule is_lub_bin_chain [THEN lub_eqI])
 done
 
-text {* continuity implies monotonicity *}
+text \<open>continuity implies monotonicity\<close>
 
 lemma cont2mono: "cont f \<Longrightarrow> monofun f"
 apply (rule monofunI)
@@ -88,7 +88,7 @@
 
 lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
 
-text {* continuity implies preservation of lubs *}
+text \<open>continuity implies preservation of lubs\<close>
 
 lemma cont2contlubE:
   "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
@@ -118,26 +118,26 @@
     by (rule thelubE)
 qed
 
-subsection {* Collection of continuity rules *}
+subsection \<open>Collection of continuity rules\<close>
 
 named_theorems cont2cont "continuity intro rule"
 
 
-subsection {* Continuity of basic functions *}
+subsection \<open>Continuity of basic functions\<close>
 
-text {* The identity function is continuous *}
+text \<open>The identity function is continuous\<close>
 
 lemma cont_id [simp, cont2cont]: "cont (\<lambda>x. x)"
 apply (rule contI)
 apply (erule cpo_lubI)
 done
 
-text {* constant functions are continuous *}
+text \<open>constant functions are continuous\<close>
 
 lemma cont_const [simp, cont2cont]: "cont (\<lambda>x. c)"
   using is_lub_const by (rule contI)
 
-text {* application of functions is continuous *}
+text \<open>application of functions is continuous\<close>
 
 lemma cont_apply:
   fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
@@ -165,7 +165,7 @@
   "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
 by (rule cont_apply [OF _ _ cont_const])
 
-text {* Least upper bounds preserve continuity *}
+text \<open>Least upper bounds preserve continuity\<close>
 
 lemma cont2cont_lub [simp]:
   assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
@@ -176,15 +176,15 @@
 apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
 done
 
-text {* if-then-else is continuous *}
+text \<open>if-then-else is continuous\<close>
 
 lemma cont_if [simp, cont2cont]:
   "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. if b then f x else g x)"
 by (induct b) simp_all
 
-subsection {* Finite chains and flat pcpos *}
+subsection \<open>Finite chains and flat pcpos\<close>
 
-text {* Monotone functions map finite chains to finite chains. *}
+text \<open>Monotone functions map finite chains to finite chains.\<close>
 
 lemma monofun_finch2finch:
   "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
@@ -193,13 +193,13 @@
 apply (force simp add: max_in_chain_def)
 done
 
-text {* The same holds for continuous functions. *}
+text \<open>The same holds for continuous functions.\<close>
 
 lemma cont_finch2finch:
   "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
 by (rule cont2mono [THEN monofun_finch2finch])
 
-text {* All monotone functions with chain-finite domain are continuous. *}
+text \<open>All monotone functions with chain-finite domain are continuous.\<close>
 
 lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
 apply (erule contI2)
@@ -210,7 +210,7 @@
 apply (force simp add: max_in_chain_def)
 done
 
-text {* All strict functions with flat domain are continuous. *}
+text \<open>All strict functions with flat domain are continuous.\<close>
 
 lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
 apply (rule monofunI)
@@ -221,7 +221,7 @@
 lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
 by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
 
-text {* All functions with discrete domain are continuous. *}
+text \<open>All functions with discrete domain are continuous.\<close>
 
 lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
 apply (rule contI)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Convex powerdomain *}
+section \<open>Convex powerdomain\<close>
 
 theory ConvexPD
 imports UpperPD LowerPD
 begin
 
-subsection {* Basis preorder *}
+subsection \<open>Basis preorder\<close>
 
 definition
   convex_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<natural>" 50) where
@@ -117,7 +117,7 @@
 done
 
 
-subsection {* Type definition *}
+subsection \<open>Type definition\<close>
 
 typedef 'a convex_pd  ("('(_')\<natural>)") =
   "{S::'a pd_basis set. convex_le.ideal S}"
@@ -150,7 +150,7 @@
 using convex_principal_def pd_basis_countable
 by (rule convex_le.typedef_ideal_completion)
 
-text {* Convex powerdomain is pointed *}
+text \<open>Convex powerdomain is pointed\<close>
 
 lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: convex_pd.principal_induct, simp, simp)
@@ -162,7 +162,7 @@
 by (rule convex_pd_minimal [THEN bottomI, symmetric])
 
 
-subsection {* Monadic unit and plus *}
+subsection \<open>Monadic unit and plus\<close>
 
 definition
   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
@@ -221,11 +221,11 @@
 lemmas convex_plus_left_commute = convex_add.left_commute
 lemmas convex_plus_left_absorb = convex_add.left_idem
 
-text {* Useful for @{text "simp add: convex_plus_ac"} *}
+text \<open>Useful for \<open>simp add: convex_plus_ac\<close>\<close>
 lemmas convex_plus_ac =
   convex_plus_assoc convex_plus_commute convex_plus_left_commute
 
-text {* Useful for @{text "simp only: convex_plus_aci"} *}
+text \<open>Useful for \<open>simp only: convex_plus_aci\<close>\<close>
 lemmas convex_plus_aci =
   convex_plus_ac convex_plus_absorb convex_plus_left_absorb
 
@@ -275,7 +275,7 @@
 by (auto dest!: convex_pd.compact_imp_principal)
 
 
-subsection {* Induction rules *}
+subsection \<open>Induction rules\<close>
 
 lemma convex_pd_induct1:
   assumes P: "adm P"
@@ -304,7 +304,7 @@
 done
 
 
-subsection {* Monadic bind *}
+subsection \<open>Monadic bind\<close>
 
 definition
   convex_bind_basis ::
@@ -376,7 +376,7 @@
 by (induct xs, simp_all)
 
 
-subsection {* Map *}
+subsection \<open>Map\<close>
 
 definition
   convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
@@ -467,7 +467,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Convex powerdomain is bifinite *}
+subsection \<open>Convex powerdomain is bifinite\<close>
 
 lemma approx_chain_convex_map:
   assumes "approx_chain a"
@@ -482,7 +482,7 @@
     by (fast intro!: approx_chain_convex_map)
 qed
 
-subsection {* Join *}
+subsection \<open>Join\<close>
 
 definition
   convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
@@ -513,9 +513,9 @@
 by (induct xss rule: convex_pd_induct, simp_all)
 
 
-subsection {* Conversions to other powerdomains *}
+subsection \<open>Conversions to other powerdomains\<close>
 
-text {* Convex to upper *}
+text \<open>Convex to upper\<close>
 
 lemma convex_le_imp_upper_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<sharp> u"
 unfolding convex_le_def by simp
@@ -555,7 +555,7 @@
     upper_bind\<cdot>(convex_to_upper\<cdot>xss)\<cdot>convex_to_upper"
 by (simp add: convex_join_def upper_join_def cfcomp_LAM eta_cfun)
 
-text {* Convex to lower *}
+text \<open>Convex to lower\<close>
 
 lemma convex_le_imp_lower_le: "t \<le>\<natural> u \<Longrightarrow> t \<le>\<flat> u"
 unfolding convex_le_def by simp
@@ -595,7 +595,7 @@
     lower_bind\<cdot>(convex_to_lower\<cdot>xss)\<cdot>convex_to_lower"
 by (simp add: convex_join_def lower_join_def cfcomp_LAM eta_cfun)
 
-text {* Ordering property *}
+text \<open>Ordering property\<close>
 
 lemma convex_pd_below_iff:
   "(xs \<sqsubseteq> ys) =
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Cpodef.thy
--- a/src/HOL/HOLCF/Cpodef.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,21 +2,21 @@
     Author:     Brian Huffman
 *)
 
-section {* Subtypes of pcpos *}
+section \<open>Subtypes of pcpos\<close>
 
 theory Cpodef
 imports Adm
 keywords "pcpodef" "cpodef" :: thy_goal
 begin
 
-subsection {* Proving a subtype is a partial order *}
+subsection \<open>Proving a subtype is a partial order\<close>
 
-text {*
+text \<open>
   A subtype of a partial order is itself a partial order,
   if the ordering is defined in the standard way.
-*}
+\<close>
 
-setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
+setup \<open>Sign.add_const_constraint (@{const_name Porder.below}, NONE)\<close>
 
 theorem typedef_po:
   fixes Abs :: "'a::po \<Rightarrow> 'b::type"
@@ -30,10 +30,10 @@
  apply (erule (1) below_antisym)
 done
 
-setup {* Sign.add_const_constraint (@{const_name Porder.below},
-  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
+setup \<open>Sign.add_const_constraint (@{const_name Porder.below},
+  SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"})\<close>
 
-subsection {* Proving a subtype is finite *}
+subsection \<open>Proving a subtype is finite\<close>
 
 lemma typedef_finite_UNIV:
   fixes Abs :: "'a::type \<Rightarrow> 'b::type"
@@ -46,7 +46,7 @@
     by (simp only: type_definition.Abs_image [OF type])
 qed
 
-subsection {* Proving a subtype is chain-finite *}
+subsection \<open>Proving a subtype is chain-finite\<close>
 
 lemma ch2ch_Rep:
   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
@@ -65,15 +65,15 @@
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
-subsection {* Proving a subtype is complete *}
+subsection \<open>Proving a subtype is complete\<close>
 
-text {*
+text \<open>
   A subtype of a cpo is itself a cpo if the ordering is
   defined in the standard way, and the defining subset
   is closed with respect to limits of chains.  A set is
   closed if and only if membership in the set is an
   admissible predicate.
-*}
+\<close>
 
 lemma typedef_is_lubI:
   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
@@ -122,9 +122,9 @@
   thus "\<exists>x. range S <<| x" ..
 qed
 
-subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
+subsubsection \<open>Continuity of \emph{Rep} and \emph{Abs}\<close>
 
-text {* For any sub-cpo, the @{term Rep} function is continuous. *}
+text \<open>For any sub-cpo, the @{term Rep} function is continuous.\<close>
 
 theorem typedef_cont_Rep:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
@@ -140,11 +140,11 @@
  apply (erule ch2ch_Rep [OF below])
 done
 
-text {*
+text \<open>
   For a sub-cpo, we can make the @{term Abs} function continuous
   only if we restrict its domain to the defining subset by
   composing it with another continuous function.
-*}
+\<close>
 
 theorem typedef_cont_Abs:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
@@ -157,7 +157,7 @@
 unfolding cont_def is_lub_def is_ub_def ball_simps below
 by (simp add: type_definition.Abs_inverse [OF type f_in_A])
 
-subsection {* Proving subtype elements are compact *}
+subsection \<open>Proving subtype elements are compact\<close>
 
 theorem typedef_compact:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
@@ -173,12 +173,12 @@
   thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
 qed
 
-subsection {* Proving a subtype is pointed *}
+subsection \<open>Proving a subtype is pointed\<close>
 
-text {*
+text \<open>
   A subtype of a cpo has a least element if and only if
   the defining subset has a least element.
-*}
+\<close>
 
 theorem typedef_pcpo_generic:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
@@ -194,10 +194,10 @@
  apply (rule z_least [OF type_definition.Rep [OF type]])
 done
 
-text {*
+text \<open>
   As a special case, a subtype of a pcpo has a least element
   if the defining subset contains @{term \<bottom>}.
-*}
+\<close>
 
 theorem typedef_pcpo:
   fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
@@ -207,12 +207,12 @@
   shows "OFCLASS('b, pcpo_class)"
 by (rule typedef_pcpo_generic [OF type below bottom_in_A], rule minimal)
 
-subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
+subsubsection \<open>Strictness of \emph{Rep} and \emph{Abs}\<close>
 
-text {*
+text \<open>
   For a sub-pcpo where @{term \<bottom>} is a member of the defining
   subset, @{term Rep} and @{term Abs} are both strict.
-*}
+\<close>
 
 theorem typedef_Abs_strict:
   assumes type: "type_definition Rep Abs A"
@@ -250,7 +250,7 @@
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
-subsection {* Proving a subtype is flat *}
+subsection \<open>Proving a subtype is flat\<close>
 
 theorem typedef_flat:
   fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
@@ -265,7 +265,7 @@
  apply (simp add: ax_flat)
 done
 
-subsection {* HOLCF type definition package *}
+subsection \<open>HOLCF type definition package\<close>
 
 ML_file "Tools/cpodef.ML"
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Cprod.thy
--- a/src/HOL/HOLCF/Cprod.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Cprod.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-section {* The cpo of cartesian products *}
+section \<open>The cpo of cartesian products\<close>
 
 theory Cprod
 imports Cfun
@@ -10,7 +10,7 @@
 
 default_sort cpo
 
-subsection {* Continuous case function for unit type *}
+subsection \<open>Continuous case function for unit type\<close>
 
 definition
   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
@@ -22,7 +22,7 @@
 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
 by (simp add: unit_when_def)
 
-subsection {* Continuous version of split function *}
+subsection \<open>Continuous version of split function\<close>
 
 definition
   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
@@ -39,7 +39,7 @@
   csnd :: "'a \<times> 'b \<rightarrow> 'b" where
   "csnd \<equiv> Abs_cfun snd"
 
-subsection {* Convert all lemmas to the continuous versions *}
+subsection \<open>Convert all lemmas to the continuous versions\<close>
 
 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
 by (simp add: csplit_def)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Deflation.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Continuous deflations and ep-pairs *}
+section \<open>Continuous deflations and ep-pairs\<close>
 
 theory Deflation
 imports Plain_HOLCF
@@ -10,7 +10,7 @@
 
 default_sort cpo
 
-subsection {* Continuous deflations *}
+subsection \<open>Continuous deflations\<close>
 
 locale deflation =
   fixes d :: "'a \<rightarrow> 'a"
@@ -21,7 +21,7 @@
 lemma below_ID: "d \<sqsubseteq> ID"
 by (rule cfun_belowI, simp add: below)
 
-text {* The set of fixed points is the same as the range. *}
+text \<open>The set of fixed points is the same as the range.\<close>
 
 lemma fixes_eq_range: "{x. d\<cdot>x = x} = range (\<lambda>x. d\<cdot>x)"
 by (auto simp add: eq_sym_conv idem)
@@ -29,10 +29,10 @@
 lemma range_eq_fixes: "range (\<lambda>x. d\<cdot>x) = {x. d\<cdot>x = x}"
 by (auto simp add: eq_sym_conv idem)
 
-text {*
+text \<open>
   The pointwise ordering on deflation functions coincides with
   the subset ordering of their sets of fixed-points.
-*}
+\<close>
 
 lemma belowI:
   assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
@@ -74,10 +74,10 @@
  apply (simp add: deflation.belowI)
 done
 
-text {*
+text \<open>
   The composition of two deflations is equal to
   the lesser of the two (if they are comparable).
-*}
+\<close>
 
 lemma deflation_below_comp1:
   assumes "deflation f"
@@ -99,7 +99,7 @@
 by (simp only: deflation.belowD deflation.idem)
 
 
-subsection {* Deflations with finite range *}
+subsection \<open>Deflations with finite range\<close>
 
 lemma finite_range_imp_finite_fixes:
   "finite (range f) \<Longrightarrow> finite {x. f x = x}"
@@ -164,7 +164,7 @@
 by standard simp_all
 
 
-subsection {* Continuous embedding-projection pairs *}
+subsection \<open>Continuous embedding-projection pairs\<close>
 
 locale ep_pair =
   fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
@@ -224,7 +224,7 @@
 lemma compact_e_iff: "compact (e\<cdot>x) \<longleftrightarrow> compact x"
 by (rule iffI [OF compact_e_rev compact_e])
 
-text {* Deflations from ep-pairs *}
+text \<open>Deflations from ep-pairs\<close>
 
 lemma deflation_e_p: "deflation (e oo p)"
 by (simp add: deflation.intro e_p_below)
@@ -321,7 +321,7 @@
 
 end
 
-subsection {* Uniqueness of ep-pairs *}
+subsection \<open>Uniqueness of ep-pairs\<close>
 
 lemma ep_pair_unique_e_lemma:
   assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
@@ -355,7 +355,7 @@
   "\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
 by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
 
-subsection {* Composing ep-pairs *}
+subsection \<open>Composing ep-pairs\<close>
 
 lemma ep_pair_ID_ID: "ep_pair ID ID"
 by standard simp_all
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Discrete.thy
--- a/src/HOL/HOLCF/Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow
 *)
 
-section {* Discrete cpo types *}
+section \<open>Discrete cpo types\<close>
 
 theory Discrete
 imports Cont
@@ -10,7 +10,7 @@
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Discrete cpo class instance *}
+subsection \<open>Discrete cpo class instance\<close>
 
 instantiation discr :: (type) discrete_cpo
 begin
@@ -23,7 +23,7 @@
 
 end
 
-subsection {* \emph{undiscr} *}
+subsection \<open>\emph{undiscr}\<close>
 
 definition
   undiscr :: "('a::type)discr => 'a" where
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Domain.thy
--- a/src/HOL/HOLCF/Domain.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Domain.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Domain package *}
+section \<open>Domain package\<close>
 
 theory Domain
 imports Representable Domain_Aux
@@ -13,7 +13,7 @@
 
 default_sort "domain"
 
-subsection {* Representations of types *}
+subsection \<open>Representations of types\<close>
 
 lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>DEFL('a)\<cdot>x"
 by (simp add: cast_DEFL)
@@ -39,7 +39,7 @@
  apply (rule monofun_cfun_arg [OF assms])
 done
 
-text {* Isomorphism lemmas used internally by the domain package: *}
+text \<open>Isomorphism lemmas used internally by the domain package:\<close>
 
 lemma domain_abs_iso:
   fixes abs and rep
@@ -59,7 +59,7 @@
 unfolding abs_def rep_def
 by (simp add: emb_prj_emb DEFL)
 
-subsection {* Deflations as sets *}
+subsection \<open>Deflations as sets\<close>
 
 definition defl_set :: "'a::bifinite defl \<Rightarrow> 'a set"
 where "defl_set A = {x. cast\<cdot>A\<cdot>x = x}"
@@ -78,11 +78,11 @@
 apply (auto simp add: cast.belowI cast.belowD)
 done
 
-subsection {* Proving a subtype is representable *}
+subsection \<open>Proving a subtype is representable\<close>
 
-text {* Temporarily relax type constraints. *}
+text \<open>Temporarily relax type constraints.\<close>
 
-setup {*
+setup \<open>
   fold Sign.add_const_constraint
   [ (@{const_name defl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom defl"})
   , (@{const_name emb}, SOME @{typ "'a::pcpo \<rightarrow> udom"})
@@ -90,7 +90,7 @@
   , (@{const_name liftdefl}, SOME @{typ "'a::pcpo itself \<Rightarrow> udom u defl"})
   , (@{const_name liftemb}, SOME @{typ "'a::pcpo u \<rightarrow> udom u"})
   , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::pcpo u"}) ]
-*}
+\<close>
 
 lemma typedef_domain_class:
   fixes Rep :: "'a::pcpo \<Rightarrow> udom"
@@ -138,9 +138,9 @@
   shows "DEFL('a::pcpo) = t"
 unfolding assms ..
 
-text {* Restore original typing constraints. *}
+text \<open>Restore original typing constraints.\<close>
 
-setup {*
+setup \<open>
   fold Sign.add_const_constraint
    [(@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"}),
     (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}),
@@ -148,11 +148,11 @@
     (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"}),
     (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
     (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"})]
-*}
+\<close>
 
 ML_file "Tools/domaindef.ML"
 
-subsection {* Isomorphic deflations *}
+subsection \<open>Isomorphic deflations\<close>
 
 definition isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> udom defl \<Rightarrow> bool"
   where "isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
@@ -314,7 +314,7 @@
 using isodefl_sfun [OF assms] unfolding isodefl_def
 by (simp add: emb_cfun_def prj_cfun_def cfcomp1 encode_cfun_map)
 
-subsection {* Setting up the domain package *}
+subsection \<open>Setting up the domain package\<close>
 
 named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
   and domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
@@ -339,7 +339,7 @@
   deflation_cfun_map deflation_sfun_map deflation_ssum_map
   deflation_sprod_map deflation_prod_map deflation_u_map
 
-setup {*
+setup \<open>
   fold Domain_Take_Proofs.add_rec_type
     [(@{type_name cfun}, [true, true]),
      (@{type_name "sfun"}, [true, true]),
@@ -347,6 +347,6 @@
      (@{type_name sprod}, [true, true]),
      (@{type_name prod}, [true, true]),
      (@{type_name "u"}, [true])]
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Domain_Aux.thy
--- a/src/HOL/HOLCF/Domain_Aux.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,15 +2,15 @@
     Author:     Brian Huffman
 *)
 
-section {* Domain package support *}
+section \<open>Domain package support\<close>
 
 theory Domain_Aux
 imports Map_Functions Fixrec
 begin
 
-subsection {* Continuous isomorphisms *}
+subsection \<open>Continuous isomorphisms\<close>
 
-text {* A locale for continuous isomorphisms *}
+text \<open>A locale for continuous isomorphisms\<close>
 
 locale iso =
   fixes abs :: "'a \<rightarrow> 'b"
@@ -108,13 +108,13 @@
 
 end
 
-subsection {* Proofs about take functions *}
+subsection \<open>Proofs about take functions\<close>
 
-text {*
+text \<open>
   This section contains lemmas that are used in a module that supports
   the domain isomorphism package; the module contains proofs related
   to take functions and the finiteness predicate.
-*}
+\<close>
 
 lemma deflation_abs_rep:
   fixes abs and rep and d
@@ -132,14 +132,14 @@
   with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
   then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
     by (rule deflation_below_comp1 [OF defl defl])
-  moreover from `m \<le> n` have "min m n = m" by simp
+  moreover from \<open>m \<le> n\<close> have "min m n = m" by simp
   ultimately show ?thesis by simp
 next
   assume "n \<le> m"
   with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
   then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
     by (rule deflation_below_comp2 [OF defl defl])
-  moreover from `n \<le> m` have "min m n = n" by simp
+  moreover from \<open>n \<le> m\<close> have "min m n = n" by simp
   ultimately show ?thesis by simp
 qed
 
@@ -164,18 +164,18 @@
   assumes "chain t" and "(\<Squnion>n. t n) = ID"
   assumes "adm P" and "\<And>n. P (t n\<cdot>x)" shows "P x"
 proof -
-  from `chain t` have "chain (\<lambda>n. t n\<cdot>x)" by simp
-  from `adm P` this `\<And>n. P (t n\<cdot>x)` have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
-  with `chain t` `(\<Squnion>n. t n) = ID` show "P x" by (simp add: lub_distribs)
+  from \<open>chain t\<close> have "chain (\<lambda>n. t n\<cdot>x)" by simp
+  from \<open>adm P\<close> this \<open>\<And>n. P (t n\<cdot>x)\<close> have "P (\<Squnion>n. t n\<cdot>x)" by (rule admD)
+  with \<open>chain t\<close> \<open>(\<Squnion>n. t n) = ID\<close> show "P x" by (simp add: lub_distribs)
 qed
 
-subsection {* Finiteness *}
+subsection \<open>Finiteness\<close>
 
-text {*
+text \<open>
   Let a ``decisive'' function be a deflation that maps every input to
   either itself or bottom.  Then if a domain's take functions are all
   decisive, then all values in the domain are finite.
-*}
+\<close>
 
 definition
   decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
@@ -252,9 +252,9 @@
   shows "(\<And>n. P (d n\<cdot>x)) \<Longrightarrow> P x"
 using lub_ID_finite [OF assms] by metis
 
-subsection {* Proofs about constructor functions *}
+subsection \<open>Proofs about constructor functions\<close>
 
-text {* Lemmas for proving nchotomy rule: *}
+text \<open>Lemmas for proving nchotomy rule:\<close>
 
 lemma ex_one_bottom_iff:
   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
@@ -290,7 +290,7 @@
    ex_up_bottom_iff
    ex_one_bottom_iff
 
-text {* Rules for turning nchotomy into exhaust: *}
+text \<open>Rules for turning nchotomy into exhaust:\<close>
 
 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
   by auto
@@ -306,7 +306,7 @@
 
 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
 
-text {* Rules for proving constructor properties *}
+text \<open>Rules for proving constructor properties\<close>
 
 lemmas con_strict_rules =
   sinl_strict sinr_strict spair_strict1 spair_strict2
@@ -342,7 +342,7 @@
   ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
   deflation_strict deflation_ID ID1 cfcomp2
 
-subsection {* ML setup *}
+subsection \<open>ML setup\<close>
 
 named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
   and domain_map_ID "theorems like foo_map$ID = ID"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-section {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
+section \<open>One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility\<close>
 
 theory Buffer_adm
 imports Buffer Stream_adm
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/FOCUS/FOCUS.thy
--- a/src/HOL/HOLCF/FOCUS/FOCUS.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-section {* Top level of FOCUS *}
+section \<open>Top level of FOCUS\<close>
 
 theory FOCUS
 imports Fstream
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -6,7 +6,7 @@
 TODO: integrate Fstreams.thy
 *)
 
-section {* FOCUS flat streams *}
+section \<open>FOCUS flat streams\<close>
 
 theory Fstream
 imports "~~/src/HOL/HOLCF/Library/Stream"
@@ -152,12 +152,12 @@
 lemma slen_fscons_eq_rev:
         "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))"
 apply (simp add: fscons_def2 slen_scons_eq_rev)
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
+apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
 apply (erule contrapos_np)
 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
 done
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/Stream_adm.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-section {* Admissibility for streams *}
+section \<open>Admissibility for streams\<close>
 
 theory Stream_adm
 imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Order_Continuity"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Fix.thy
--- a/src/HOL/HOLCF/Fix.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Fix.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Fixed point operator and admissibility *}
+section \<open>Fixed point operator and admissibility\<close>
 
 theory Fix
 imports Cfun
@@ -11,13 +11,13 @@
 
 default_sort pcpo
 
-subsection {* Iteration *}
+subsection \<open>Iteration\<close>
 
 primrec iterate :: "nat \<Rightarrow> ('a::cpo \<rightarrow> 'a) \<rightarrow> ('a \<rightarrow> 'a)" where
     "iterate 0 = (\<Lambda> F x. x)"
   | "iterate (Suc n) = (\<Lambda> F x. F\<cdot>(iterate n\<cdot>F\<cdot>x))"
 
-text {* Derive inductive properties of iterate from primitive recursion *}
+text \<open>Derive inductive properties of iterate from primitive recursion\<close>
 
 lemma iterate_0 [simp]: "iterate 0\<cdot>F\<cdot>x = x"
 by simp
@@ -34,19 +34,19 @@
   "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x"
 by (induct m) simp_all
 
-text {* The sequence of function iterations is a chain. *}
+text \<open>The sequence of function iterations is a chain.\<close>
 
 lemma chain_iterate [simp]: "chain (\<lambda>i. iterate i\<cdot>F\<cdot>\<bottom>)"
 by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)
 
 
-subsection {* Least fixed point operator *}
+subsection \<open>Least fixed point operator\<close>
 
 definition
   "fix" :: "('a \<rightarrow> 'a) \<rightarrow> 'a" where
   "fix = (\<Lambda> F. \<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
 
-text {* Binder syntax for @{term fix} *}
+text \<open>Binder syntax for @{term fix}\<close>
 
 abbreviation
   fix_syn :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  (binder "\<mu> " 10) where
@@ -55,9 +55,9 @@
 notation (ASCII)
   fix_syn  (binder "FIX " 10)
 
-text {* Properties of @{term fix} *}
+text \<open>Properties of @{term fix}\<close>
 
-text {* direct connection between @{term fix} and iteration *}
+text \<open>direct connection between @{term fix} and iteration\<close>
 
 lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
 unfolding fix_def by simp
@@ -66,10 +66,10 @@
   unfolding fix_def2
   using chain_iterate by (rule is_ub_thelub)
 
-text {*
+text \<open>
   Kleene's fixed point theorems for continuous functions in pointed
   omega cpo's
-*}
+\<close>
 
 lemma fix_eq: "fix\<cdot>F = F\<cdot>(fix\<cdot>F)"
 apply (simp add: fix_def2)
@@ -116,7 +116,7 @@
 lemma fix_eq5: "f = fix\<cdot>F \<Longrightarrow> f\<cdot>x = F\<cdot>f\<cdot>x"
 by (erule fix_eq4 [THEN cfun_fun_cong])
 
-text {* strictness of @{term fix} *}
+text \<open>strictness of @{term fix}\<close>
 
 lemma fix_bottom_iff: "(fix\<cdot>F = \<bottom>) = (F\<cdot>\<bottom> = \<bottom>)"
 apply (rule iffI)
@@ -131,7 +131,7 @@
 lemma fix_defined: "F\<cdot>\<bottom> \<noteq> \<bottom> \<Longrightarrow> fix\<cdot>F \<noteq> \<bottom>"
 by (simp add: fix_bottom_iff)
 
-text {* @{term fix} applied to identity and constant functions *}
+text \<open>@{term fix} applied to identity and constant functions\<close>
 
 lemma fix_id: "(\<mu> x. x) = \<bottom>"
 by (simp add: fix_strict)
@@ -139,7 +139,7 @@
 lemma fix_const: "(\<mu> x. c) = c"
 by (subst fix_eq, simp)
 
-subsection {* Fixed point induction *}
+subsection \<open>Fixed point induction\<close>
 
 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
 unfolding fix_def2
@@ -202,12 +202,12 @@
   shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))"
 by (rule parallel_fix_ind, simp_all add: assms)
 
-subsection {* Fixed-points on product types *}
+subsection \<open>Fixed-points on product types\<close>
 
-text {*
+text \<open>
   Bekic's Theorem: Simultaneous fixed points over pairs
   can be written in terms of separate fixed points.
-*}
+\<close>
 
 lemma fix_cprod:
   "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -9,7 +9,7 @@
 keywords "fixrec" :: thy_decl
 begin
 
-subsection {* Pattern-match monad *}
+subsection \<open>Pattern-match monad\<close>
 
 default_sort cpo
 
@@ -46,13 +46,13 @@
   "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
 
-subsubsection {* Run operator *}
+subsubsection \<open>Run operator\<close>
 
 definition
   run :: "'a match \<rightarrow> 'a::pcpo" where
   "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))"
 
-text {* rewrite rules for run *}
+text \<open>rewrite rules for run\<close>
 
 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>"
 unfolding run_def
@@ -66,7 +66,7 @@
 unfolding run_def succeed_def
 by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
 
-subsubsection {* Monad plus operator *}
+subsubsection \<open>Monad plus operator\<close>
 
 definition
   mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where
@@ -76,7 +76,7 @@
   mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr "+++" 65)  where
   "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
 
-text {* rewrite rules for mplus *}
+text \<open>rewrite rules for mplus\<close>
 
 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
 unfolding mplus_def
@@ -96,7 +96,7 @@
 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
 by (cases x, simp_all)
 
-subsection {* Match functions for built-in types *}
+subsection \<open>Match functions for built-in types\<close>
 
 default_sort pcpo
 
@@ -192,12 +192,12 @@
   "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_FF_def)
 
-subsection {* Mutual recursion *}
+subsection \<open>Mutual recursion\<close>
 
-text {*
+text \<open>
   The following rules are used to prove unfolding theorems from
   fixed-point definitions of mutually recursive functions.
-*}
+\<close>
 
 lemma Pair_equalI: "\<lbrakk>x \<equiv> fst p; y \<equiv> snd p\<rbrakk> \<Longrightarrow> (x, y) \<equiv> p"
 by simp
@@ -216,22 +216,22 @@
   "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
 by (simp add: fix_ind)
 
-text {* lemma for proving rewrite rules *}
+text \<open>lemma for proving rewrite rules\<close>
 
 lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
 by simp
 
 
-subsection {* Initializing the fixrec package *}
+subsection \<open>Initializing the fixrec package\<close>
 
 ML_file "Tools/holcf_library.ML"
 ML_file "Tools/fixrec.ML"
 
-method_setup fixrec_simp = {*
+method_setup fixrec_simp = \<open>
   Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
-*} "pattern prover for fixrec constants"
+\<close> "pattern prover for fixrec constants"
 
-setup {*
+setup \<open>
   Fixrec.add_matchers
     [ (@{const_name up}, @{const_name match_up}),
       (@{const_name sinl}, @{const_name match_sinl}),
@@ -242,7 +242,7 @@
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),
       (@{const_name bottom}, @{const_name match_bottom}) ]
-*}
+\<close>
 
 hide_const (open) succeed fail run
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Fun_Cpo.thy
--- a/src/HOL/HOLCF/Fun_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Fun_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,13 +3,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Class instances for the full function space *}
+section \<open>Class instances for the full function space\<close>
 
 theory Fun_Cpo
 imports Adm
 begin
 
-subsection {* Full function space is a partial order *}
+subsection \<open>Full function space is a partial order\<close>
 
 instantiation "fun"  :: (type, below) below
 begin
@@ -44,9 +44,9 @@
 lemma fun_belowD: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
 by (simp add: below_fun_def)
 
-subsection {* Full function space is chain complete *}
+subsection \<open>Full function space is chain complete\<close>
 
-text {* Properties of chains of functions. *}
+text \<open>Properties of chains of functions.\<close>
 
 lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
 unfolding chain_def fun_below_iff by auto
@@ -57,7 +57,7 @@
 lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
 by (simp add: chain_def below_fun_def)
 
-text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
+text \<open>Type @{typ "'a::type => 'b::cpo"} is chain complete\<close>
 
 lemma is_lub_lambda:
   "(\<And>x. range (\<lambda>i. Y i x) <<| f x) \<Longrightarrow> range Y <<| f"
@@ -87,7 +87,7 @@
     by simp
 qed
 
-subsection {* Full function space is pointed *}
+subsection \<open>Full function space is pointed\<close>
 
 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
 by (simp add: below_fun_def)
@@ -104,19 +104,19 @@
 lemma lambda_strict: "(\<lambda>x. \<bottom>) = \<bottom>"
 by (rule bottomI, rule minimal_fun)
 
-subsection {* Propagation of monotonicity and continuity *}
+subsection \<open>Propagation of monotonicity and continuity\<close>
 
-text {* The lub of a chain of monotone functions is monotone. *}
+text \<open>The lub of a chain of monotone functions is monotone.\<close>
 
 lemma adm_monofun: "adm monofun"
 by (rule admI, simp add: lub_fun fun_chain_iff monofun_def lub_mono)
 
-text {* The lub of a chain of continuous functions is continuous. *}
+text \<open>The lub of a chain of continuous functions is continuous.\<close>
 
 lemma adm_cont: "adm cont"
 by (rule admI, simp add: lub_fun fun_chain_iff)
 
-text {* Function application preserves monotonicity and continuity. *}
+text \<open>Function application preserves monotonicity and continuity.\<close>
 
 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
 by (simp add: monofun_def fun_below_iff)
@@ -130,10 +130,10 @@
 lemma cont_fun: "cont (\<lambda>f. f x)"
 using cont_id by (rule cont2cont_fun)
 
-text {*
+text \<open>
   Lambda abstraction preserves monotonicity and continuity.
-  (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)
-*}
+  (Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)
+\<close>
 
 lemma mono2mono_lambda:
   assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
@@ -143,7 +143,7 @@
   assumes f: "\<And>y. cont (\<lambda>x. f x y)" shows "cont f"
 by (rule contI, rule is_lub_lambda, rule contE [OF f])
 
-text {* What D.A.Schmidt calls continuity of abstraction; never used here *}
+text \<open>What D.A.Schmidt calls continuity of abstraction; never used here\<close>
 
 lemma contlub_lambda:
   "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo))
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/IMP/HoareEx.thy
--- a/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -7,11 +7,11 @@
 
 theory HoareEx imports Denotational begin
 
-text {*
+text \<open>
   An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
   @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
   the correctness of the Hoare rule for while-loops.
-*}
+\<close>
 
 type_synonym assn = "state => bool"
 
@@ -24,7 +24,7 @@
   apply (unfold hoare_valid_def)
   apply (simp (no_asm))
   apply (rule fix_ind)
-    apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic"
+    apply (simp (no_asm)) \<comment> "simplifier with enhanced \<open>adm\<close>-tactic"
    apply (simp (no_asm))
   apply (simp (no_asm))
   apply blast
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Bool_Discrete.thy
--- a/src/HOL/HOLCF/Library/Bool_Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Discrete cpo instance for booleans *}
+section \<open>Discrete cpo instance for booleans\<close>
 
 theory Bool_Discrete
 imports HOLCF
 begin
 
-text {* Discrete cpo instance for @{typ bool}. *}
+text \<open>Discrete cpo instance for @{typ bool}.\<close>
 
 instantiation bool :: discrete_cpo
 begin
@@ -21,9 +21,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation bool :: predomain
 begin
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Char_Discrete.thy
--- a/src/HOL/HOLCF/Library/Char_Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Discrete cpo instance for 8-bit char type *}
+section \<open>Discrete cpo instance for 8-bit char type\<close>
 
 theory Char_Discrete
 imports HOLCF
 begin
 
-subsection {* Discrete cpo instance for @{typ nibble}. *}
+subsection \<open>Discrete cpo instance for @{typ nibble}.\<close>
 
 instantiation nibble :: discrete_cpo
 begin
@@ -21,9 +21,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation nibble :: predomain
 begin
@@ -54,7 +54,7 @@
 
 end
 
-subsection {* Discrete cpo instance for @{typ char}. *}
+subsection \<open>Discrete cpo instance for @{typ char}.\<close>
 
 instantiation char :: discrete_cpo
 begin
@@ -67,9 +67,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation char :: predomain
 begin
@@ -100,7 +100,7 @@
 
 end
 
-subsection {* Using chars with Fixrec *}
+subsection \<open>Using chars with Fixrec\<close>
 
 definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match"
   where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)"
@@ -221,7 +221,7 @@
   "match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)"
 by (simp add: match_NibbleF_def)
 
-setup {*
+setup \<open>
   Fixrec.add_matchers
     [ (@{const_name Char}, @{const_name match_Char}),
       (@{const_name Nibble0}, @{const_name match_Nibble0}),
@@ -240,6 +240,6 @@
       (@{const_name NibbleD}, @{const_name match_NibbleD}),
       (@{const_name NibbleE}, @{const_name match_NibbleE}),
       (@{const_name NibbleF}, @{const_name match_NibbleF}) ]
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,17 +2,17 @@
     Author:     Brian Huffman
 *)
 
-section {* Algebraic deflations are a bifinite domain *}
+section \<open>Algebraic deflations are a bifinite domain\<close>
 
 theory Defl_Bifinite
 imports HOLCF "~~/src/HOL/Library/Infinite_Set"
 begin
 
-subsection {* Lemmas about MOST *}
+subsection \<open>Lemmas about MOST\<close>
 
 default_sort type
 
-subsection {* Eventually constant sequences *}
+subsection \<open>Eventually constant sequences\<close>
 
 definition
   eventually_constant :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool"
@@ -48,7 +48,7 @@
   "eventually_constant (\<lambda>i. S (Suc i)) \<Longrightarrow> eventually_constant (\<lambda>i. S i)"
 by (rule eventually_constant_Suc_iff [THEN iffD1])
 
-subsection {* Limits of eventually constant sequences *}
+subsection \<open>Limits of eventually constant sequences\<close>
 
 definition
   eventual :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -120,7 +120,7 @@
 apply simp
 done
 
-subsection {* Constructing finite deflations by iteration *}
+subsection \<open>Constructing finite deflations by iteration\<close>
 
 default_sort cpo
 
@@ -144,7 +144,7 @@
 where
   "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
 
-text {* A pre-deflation is like a deflation, but not idempotent. *}
+text \<open>A pre-deflation is like a deflation, but not idempotent.\<close>
 
 locale pre_deflation =
   fixes f :: "'a \<rightarrow> 'a::cpo"
@@ -301,7 +301,7 @@
   interpret d: finite_deflation d by fact
   let ?e = "d oo f"
   interpret e: pre_deflation "d oo f"
-    using `finite_deflation d` f
+    using \<open>finite_deflation d\<close> f
     by (rule pre_deflation_oo)
   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
   show ?thesis
@@ -338,7 +338,7 @@
 apply (rule eventual_mono)
 apply (rule pre_deflation.eventually_constant_iterate [OF f])
 apply (rule pre_deflation.eventually_constant_iterate [OF g])
-apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
+apply (rule monofun_cfun_arg [OF \<open>f \<sqsubseteq> g\<close>])
 done
 
 lemma cont2cont_eventual_iterate_oo:
@@ -380,15 +380,15 @@
     have "compact (d\<cdot>x)"
       using d by (rule finite_deflation.compact)
     then have "compact x"
-      using `d\<cdot>x = x` by simp
+      using \<open>d\<cdot>x = x\<close> by simp
     then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
-      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
+      using \<open>(\<Squnion>i. f (Y i)\<cdot>x) = x\<close> by simp
     then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
       by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
     then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
     then have "f (Y n)\<cdot>x = x"
-      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
-    with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
+      using \<open>(\<Squnion>i. f (Y i)\<cdot>x) = x\<close> fY by (simp add: maxinch_is_thelub)
+    with \<open>d\<cdot>x = x\<close> have "?e (Y n)\<cdot>x = x"
       by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
     moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
       by (rule is_ub_thelub, simp add: eY)
@@ -404,7 +404,7 @@
   qed
 qed
 
-subsection {* Intersection of algebraic deflations *}
+subsection \<open>Intersection of algebraic deflations\<close>
 
 default_sort bifinite
 
@@ -545,7 +545,7 @@
 lemma compact_meet_defl2: "compact b \<Longrightarrow> compact (meet_defl\<cdot>a\<cdot>b)"
 by (subst meet_defl.commute, rule compact_meet_defl1)
 
-subsection {* Chain of approx functions on algebraic deflations *}
+subsection \<open>Chain of approx functions on algebraic deflations\<close>
 
 context bifinite_approx_chain
 begin
@@ -587,7 +587,7 @@
 
 end
 
-subsection {* Algebraic deflations are a bifinite domain *}
+subsection \<open>Algebraic deflations are a bifinite domain\<close>
 
 instance defl :: (bifinite) bifinite
 proof
@@ -599,7 +599,7 @@
     by (fast intro: bifinite_approx_chain.defl_approx)
 qed
 
-subsection {* Algebraic deflations are representable *}
+subsection \<open>Algebraic deflations are representable\<close>
 
 default_sort "domain"
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/HOL_Cpo.thy
--- a/src/HOL/HOLCF/Library/HOL_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Cpo class instances for all HOL types *}
+section \<open>Cpo class instances for all HOL types\<close>
 
 theory HOL_Cpo
 imports
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Int_Discrete.thy
--- a/src/HOL/HOLCF/Library/Int_Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Discrete cpo instance for integers *}
+section \<open>Discrete cpo instance for integers\<close>
 
 theory Int_Discrete
 imports HOLCF
 begin
 
-text {* Discrete cpo instance for @{typ int}. *}
+text \<open>Discrete cpo instance for @{typ int}.\<close>
 
 instantiation int :: discrete_cpo
 begin
@@ -21,9 +21,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation int :: predomain
 begin
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Lists as a complete partial order *}
+section \<open>Lists as a complete partial order\<close>
 
 theory List_Cpo
 imports HOLCF
 begin
 
-subsection {* Lists are a partial order *}
+subsection \<open>Lists are a partial order\<close>
 
 instantiation list :: (po) po
 begin
@@ -55,7 +55,7 @@
   assumes 1: "P [] []"
   assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
   shows "P xs ys"
-using `xs \<sqsubseteq> ys`
+using \<open>xs \<sqsubseteq> ys\<close>
 proof (induct xs arbitrary: ys)
   case Nil thus ?case by (simp add: 1)
 next
@@ -100,20 +100,20 @@
   assumes 1: "P (\<lambda>i. [])"
   assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)"
   shows "P S"
-using `chain S`
+using \<open>chain S\<close>
 proof (induct "S 0" arbitrary: S)
   case Nil
-  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
+  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>])
   with Nil have "\<forall>i. S i = []" by simp
   thus ?case by (simp add: 1)
 next
   case (Cons x xs)
-  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`])
+  have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>])
   hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto
   have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))"
-    using `chain S` by simp_all
+    using \<open>chain S\<close> by simp_all
   moreover have "P (\<lambda>i. tl (S i))"
-    using `chain S` and `x # xs = S 0` [symmetric]
+    using \<open>chain S\<close> and \<open>x # xs = S 0\<close> [symmetric]
     by (simp add: Cons(1))
   ultimately have "P (\<lambda>i. hd (S i) # tl (S i))"
     by (rule 2)
@@ -126,7 +126,7 @@
     A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)"
 using S by (induct rule: list_chain_induct) simp_all
 
-subsection {* Lists are a complete partial order *}
+subsection \<open>Lists are a complete partial order\<close>
 
 lemma is_lub_Cons:
   assumes A: "range A <<| x"
@@ -147,7 +147,7 @@
   qed
 qed
 
-subsection {* Continuity of list operations *}
+subsection \<open>Continuity of list operations\<close>
 
 lemma cont2cont_Cons [simp, cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
@@ -193,8 +193,8 @@
   shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
 using assms by (simp add: cont2cont_case_list prod_cont_iff)
 
-text {* The simple version (due to Joachim Breitner) is needed if the
-  element type of the list is not a cpo. *}
+text \<open>The simple version (due to Joachim Breitner) is needed if the
+  element type of the list is not a cpo.\<close>
 
 lemma cont2cont_case_list_simple [simp, cont2cont]:
   assumes "cont (\<lambda>x. f1 x)"
@@ -202,7 +202,7 @@
   shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
 using assms by (cases l) auto
 
-text {* Lemma for proving continuity of recursive list functions: *}
+text \<open>Lemma for proving continuity of recursive list functions:\<close>
 
 lemma list_contI:
   fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo"
@@ -233,7 +233,7 @@
     done
 qed
 
-text {* Continuity rule for map *}
+text \<open>Continuity rule for map\<close>
 
 lemma cont2cont_map [simp, cont2cont]:
   assumes f: "cont (\<lambda>(x, y). f x y)"
@@ -246,11 +246,11 @@
 apply (induct_tac y, simp, simp)
 done
 
-text {* There are probably lots of other list operations that also
+text \<open>There are probably lots of other list operations that also
 deserve to have continuity lemmas.  I'll add more as they are
-needed. *}
+needed.\<close>
 
-subsection {* Lists are a discrete cpo *}
+subsection \<open>Lists are a discrete cpo\<close>
 
 instance list :: (discrete_cpo) discrete_cpo
 proof
@@ -259,7 +259,7 @@
     by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
 qed
 
-subsection {* Compactness and chain-finiteness *}
+subsection \<open>Compactness and chain-finiteness\<close>
 
 lemma compact_Nil [simp]: "compact []"
 apply (rule compactI2)
@@ -298,7 +298,7 @@
     by (rule compact_imp_max_in_chain)
 qed
 
-subsection {* Using lists with fixrec *}
+subsection \<open>Using lists with fixrec\<close>
 
 definition
   match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
@@ -320,10 +320,10 @@
   "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
 unfolding match_Cons_def by simp_all
 
-setup {*
+setup \<open>
   Fixrec.add_matchers
     [ (@{const_name Nil}, @{const_name match_Nil}),
       (@{const_name Cons}, @{const_name match_Cons}) ]
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/List_Predomain.thy
--- a/src/HOL/HOLCF/Library/List_Predomain.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,19 +2,19 @@
     Author:     Brian Huffman
 *)
 
-section {* Predomain class instance for HOL list type *}
+section \<open>Predomain class instance for HOL list type\<close>
 
 theory List_Predomain
 imports List_Cpo Sum_Cpo
 begin
 
-subsection {* Strict list type *}
+subsection \<open>Strict list type\<close>
 
 domain 'a slist = SNil | SCons "'a" "'a slist"
 
-text {* Polymorphic map function for strict lists. *}
+text \<open>Polymorphic map function for strict lists.\<close>
 
-text {* FIXME: The domain package should generate this! *}
+text \<open>FIXME: The domain package should generate this!\<close>
 
 fixrec slist_map' :: "('a \<rightarrow> 'b) \<rightarrow> 'a slist \<rightarrow> 'b slist"
   where "slist_map'\<cdot>f\<cdot>SNil = SNil"
@@ -60,9 +60,9 @@
 apply (simp add: cfun_below_iff ep_pair.e_p_below)
 done
 
-text {*
+text \<open>
   Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
-*}
+\<close>
 
 fixrec encode_list_u where
   "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
@@ -94,7 +94,7 @@
 apply (case_tac "decode_list_u\<cdot>y", simp, simp)
 done
 
-subsection {* Lists are a predomain *}
+subsection \<open>Lists are a predomain\<close>
 
 definition list_liftdefl :: "udom u defl \<rightarrow> udom u defl"
   where "list_liftdefl = (\<Lambda> a. udefl\<cdot>(slist_defl\<cdot>(u_liftdefl\<cdot>a)))"
@@ -129,7 +129,7 @@
 
 end
 
-subsection {* Configuring domain package to work with list type *}
+subsection \<open>Configuring domain package to work with list type\<close>
 
 lemma liftdefl_list [domain_defl_simps]:
   "LIFTDEFL('a::predomain list) = list_liftdefl\<cdot>LIFTDEFL('a)"
@@ -167,8 +167,8 @@
 apply (simp add: slist_map'_slist_map' u_emb_bottom)
 done
 
-setup {*
+setup \<open>
   Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Nat_Discrete.thy
--- a/src/HOL/HOLCF/Library/Nat_Discrete.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Discrete cpo instance for naturals *}
+section \<open>Discrete cpo instance for naturals\<close>
 
 theory Nat_Discrete
 imports HOLCF
 begin
 
-text {* Discrete cpo instance for @{typ nat}. *}
+text \<open>Discrete cpo instance for @{typ nat}.\<close>
 
 instantiation nat :: discrete_cpo
 begin
@@ -21,9 +21,9 @@
 
 end
 
-text {*
+text \<open>
   TODO: implement a command to automate discrete predomain instances.
-*}
+\<close>
 
 instantiation nat :: predomain
 begin
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Option_Cpo.thy
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Cpo class instance for HOL option type *}
+section \<open>Cpo class instance for HOL option type\<close>
 
 theory Option_Cpo
 imports HOLCF Sum_Cpo
 begin
 
-subsection {* Ordering on option type *}
+subsection \<open>Ordering on option type\<close>
 
 instantiation option :: (below) below
 begin
@@ -49,7 +49,7 @@
 using assms unfolding below_option_def
 by (simp split: option.split_asm)
 
-subsection {* Option type is a complete partial order *}
+subsection \<open>Option type is a complete partial order\<close>
 
 instance option :: (po) po
 proof
@@ -106,7 +106,7 @@
  apply (erule cpo_lubI)
 done
 
-subsection {* Continuity of Some and case function *}
+subsection \<open>Continuity of Some and case function\<close>
 
 lemma cont_Some: "cont Some"
 by (intro contI is_lub_Some cpo_lubI)
@@ -141,7 +141,7 @@
   shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
 using assms by (simp add: cont2cont_case_option prod_cont_iff)
 
-text {* Simple version for when the element type is not a cpo. *}
+text \<open>Simple version for when the element type is not a cpo.\<close>
 
 lemma cont2cont_case_option_simple [simp, cont2cont]:
   assumes "cont (\<lambda>x. f x)"
@@ -149,7 +149,7 @@
   shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
 using assms by (cases z) auto
 
-text {* Continuity rule for map. *}
+text \<open>Continuity rule for map.\<close>
 
 lemma cont2cont_map_option [simp, cont2cont]:
   assumes f: "cont (\<lambda>(x, y). f x y)"
@@ -157,7 +157,7 @@
   shows "cont (\<lambda>x. map_option (\<lambda>y. f x y) (g x))"
 using assms by (simp add: prod_cont_iff map_option_case)
 
-subsection {* Compactness and chain-finiteness *}
+subsection \<open>Compactness and chain-finiteness\<close>
 
 lemma compact_None [simp]: "compact None"
 apply (rule compactI2)
@@ -190,7 +190,7 @@
 instance option :: (discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_option_def split: option.split)
 
-subsection {* Using option types with Fixrec *}
+subsection \<open>Using option types with Fixrec\<close>
 
 definition
   "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"
@@ -208,13 +208,13 @@
   "match_Some\<cdot>(Some a)\<cdot>k = k\<cdot>a"
 unfolding match_Some_def by simp_all
 
-setup {*
+setup \<open>
   Fixrec.add_matchers
     [ (@{const_name None}, @{const_name match_None}),
       (@{const_name Some}, @{const_name match_Some}) ]
-*}
+\<close>
 
-subsection {* Option type is a predomain *}
+subsection \<open>Option type is a predomain\<close>
 
 definition
   "encode_option = (\<Lambda> x. case x of None \<Rightarrow> Inl () | Some a \<Rightarrow> Inr a)"
@@ -255,7 +255,7 @@
 
 end
 
-subsection {* Configuring domain package to work with option type *}
+subsection \<open>Configuring domain package to work with option type\<close>
 
 lemma liftdefl_option [domain_defl_simps]:
   "LIFTDEFL('a::predomain option) = LIFTDEFL(unit + 'a)"
@@ -285,8 +285,8 @@
 unfolding isodefl'_def liftemb_option_def liftprj_option_def liftdefl_eq
 by (simp add: cfcomp1 u_map_map encode_option_option_map)
 
-setup {*
+setup \<open>
   Domain_Take_Proofs.add_rec_type (@{type_name "option"}, [true])
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Stream.thy
--- a/src/HOL/HOLCF/Library/Stream.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Stream.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
 *)
 
-section {* General Stream domain *}
+section \<open>General Stream domain\<close>
 
 theory Stream
 imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* The cpo of disjoint sums *}
+section \<open>The cpo of disjoint sums\<close>
 
 theory Sum_Cpo
 imports HOLCF
 begin
 
-subsection {* Ordering on sum type *}
+subsection \<open>Ordering on sum type\<close>
 
 instantiation sum :: (below, below) below
 begin
@@ -54,7 +54,7 @@
       \<Longrightarrow> R"
 by (cases x, safe elim!: sum_below_elims, auto)
 
-subsection {* Sum type is a complete partial order *}
+subsection \<open>Sum type is a complete partial order\<close>
 
 instance sum :: (po, po) po
 proof
@@ -128,7 +128,7 @@
  apply (erule cpo_lubI)
 done
 
-subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
+subsection \<open>Continuity of \emph{Inl}, \emph{Inr}, and case function\<close>
 
 lemma cont_Inl: "cont Inl"
 by (intro contI is_lub_Inl cpo_lubI)
@@ -175,7 +175,7 @@
   shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
 using assms by (simp add: cont2cont_case_sum prod_cont_iff)
 
-text {* Continuity of map function. *}
+text \<open>Continuity of map function.\<close>
 
 lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
 by (rule ext, case_tac x, simp_all)
@@ -187,7 +187,7 @@
   shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
 using assms by (simp add: map_sum_eq prod_cont_iff)
 
-subsection {* Compactness and chain-finiteness *}
+subsection \<open>Compactness and chain-finiteness\<close>
 
 lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
 apply (rule compactI2)
@@ -228,7 +228,7 @@
 instance sum :: (discrete_cpo, discrete_cpo) discrete_cpo
 by intro_classes (simp add: below_sum_def split: sum.split)
 
-subsection {* Using sum types with fixrec *}
+subsection \<open>Using sum types with fixrec\<close>
 
 definition
   "match_Inl = (\<Lambda> x k. case x of Inl a \<Rightarrow> k\<cdot>a | Inr b \<Rightarrow> Fixrec.fail)"
@@ -246,13 +246,13 @@
   "match_Inr\<cdot>(Inr b)\<cdot>k = k\<cdot>b"
 unfolding match_Inr_def by simp_all
 
-setup {*
+setup \<open>
   Fixrec.add_matchers
     [ (@{const_name Inl}, @{const_name match_Inl}),
       (@{const_name Inr}, @{const_name match_Inr}) ]
-*}
+\<close>
 
-subsection {* Disjoint sum is a predomain *}
+subsection \<open>Disjoint sum is a predomain\<close>
 
 definition
   "encode_sum_u =
@@ -272,7 +272,7 @@
 apply (rename_tac b, case_tac b, simp, simp)
 done
 
-text {* A deflation combinator for making unpointed types *}
+text \<open>A deflation combinator for making unpointed types\<close>
 
 definition udefl :: "udom defl \<rightarrow> udom u defl"
   where "udefl = defl_fun1 (strictify\<cdot>up) (fup\<cdot>ID) ID"
@@ -327,7 +327,7 @@
 
 end
 
-subsection {* Configuring domain package to work with sum type *}
+subsection \<open>Configuring domain package to work with sum type\<close>
 
 lemma liftdefl_sum [domain_defl_simps]:
   "LIFTDEFL('a::predomain + 'b::predomain) =
@@ -365,8 +365,8 @@
 apply (simp add: ssum_map_map u_emb_bottom)
 done
 
-setup {*
+setup \<open>
   Domain_Take_Proofs.add_rec_type (@{type_name "sum"}, [true, true])
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Mueller
 *)
 
-section {* Lifting types of class type to flat pcpo's *}
+section \<open>Lifting types of class type to flat pcpo's\<close>
 
 theory Lift
 imports Discrete Up
@@ -19,7 +19,7 @@
   Def :: "'a \<Rightarrow> 'a lift" where
   "Def x = Abs_lift (up\<cdot>(Discr x))"
 
-subsection {* Lift as a datatype *}
+subsection \<open>Lift as a datatype\<close>
 
 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
 apply (induct y)
@@ -32,7 +32,7 @@
 old_rep_datatype "\<bottom>::'a lift" Def
   by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
 
-text {* @{term bottom} and @{term Def} *}
+text \<open>@{term bottom} and @{term Def}\<close>
 
 lemma not_Undef_is_Def: "(x \<noteq> \<bottom>) = (\<exists>y. x = Def y)"
   by (cases x) simp_all
@@ -40,14 +40,13 @@
 lemma lift_definedE: "\<lbrakk>x \<noteq> \<bottom>; \<And>a. x = Def a \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   by (cases x) simp_all
 
-text {*
-  For @{term "x ~= \<bottom>"} in assumptions @{text defined} replaces @{text
-  x} by @{text "Def a"} in conclusion. *}
+text \<open>
+  For @{term "x ~= \<bottom>"} in assumptions \<open>defined\<close> replaces \<open>x\<close> by \<open>Def a\<close> in conclusion.\<close>
 
-method_setup defined = {*
+method_setup defined = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD'
     (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt))
-*}
+\<close>
 
 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
   by simp
@@ -62,7 +61,7 @@
 by (induct y, simp, simp add: Def_below_Def)
 
 
-subsection {* Lift is flat *}
+subsection \<open>Lift is flat\<close>
 
 instance lift :: (type) flat
 proof
@@ -71,7 +70,7 @@
     by (induct x) auto
 qed
 
-subsection {* Continuity of @{const case_lift} *}
+subsection \<open>Continuity of @{const case_lift}\<close>
 
 lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
 apply (induct x, unfold lift.case)
@@ -83,7 +82,7 @@
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
 unfolding case_lift_eq by (simp add: cont_Rep_lift)
 
-subsection {* Further operations *}
+subsection \<open>Further operations\<close>
 
 definition
   flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Lower powerdomain *}
+section \<open>Lower powerdomain\<close>
 
 theory LowerPD
 imports Compact_Basis
 begin
 
-subsection {* Basis preorder *}
+subsection \<open>Basis preorder\<close>
 
 definition
   lower_le :: "'a pd_basis \<Rightarrow> 'a pd_basis \<Rightarrow> bool" (infix "\<le>\<flat>" 50) where
@@ -72,7 +72,7 @@
 done
 
 
-subsection {* Type definition *}
+subsection \<open>Type definition\<close>
 
 typedef 'a lower_pd  ("('(_')\<flat>)") =
   "{S::'a pd_basis set. lower_le.ideal S}"
@@ -105,7 +105,7 @@
 using lower_principal_def pd_basis_countable
 by (rule lower_le.typedef_ideal_completion)
 
-text {* Lower powerdomain is pointed *}
+text \<open>Lower powerdomain is pointed\<close>
 
 lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: lower_pd.principal_induct, simp, simp)
@@ -117,7 +117,7 @@
 by (rule lower_pd_minimal [THEN bottomI, symmetric])
 
 
-subsection {* Monadic unit and plus *}
+subsection \<open>Monadic unit and plus\<close>
 
 definition
   lower_unit :: "'a \<rightarrow> 'a lower_pd" where
@@ -176,11 +176,11 @@
 lemmas lower_plus_left_commute = lower_add.left_commute
 lemmas lower_plus_left_absorb = lower_add.left_idem
 
-text {* Useful for @{text "simp add: lower_plus_ac"} *}
+text \<open>Useful for \<open>simp add: lower_plus_ac\<close>\<close>
 lemmas lower_plus_ac =
   lower_plus_assoc lower_plus_commute lower_plus_left_commute
 
-text {* Useful for @{text "simp only: lower_plus_aci"} *}
+text \<open>Useful for \<open>simp only: lower_plus_aci\<close>\<close>
 lemmas lower_plus_aci =
   lower_plus_ac lower_plus_absorb lower_plus_left_absorb
 
@@ -267,7 +267,7 @@
 by (auto dest!: lower_pd.compact_imp_principal)
 
 
-subsection {* Induction rules *}
+subsection \<open>Induction rules\<close>
 
 lemma lower_pd_induct1:
   assumes P: "adm P"
@@ -297,7 +297,7 @@
 done
 
 
-subsection {* Monadic bind *}
+subsection \<open>Monadic bind\<close>
 
 definition
   lower_bind_basis ::
@@ -369,7 +369,7 @@
 by (induct xs, simp_all)
 
 
-subsection {* Map *}
+subsection \<open>Map\<close>
 
 definition
   lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
@@ -460,7 +460,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-subsection {* Lower powerdomain is bifinite *}
+subsection \<open>Lower powerdomain is bifinite\<close>
 
 lemma approx_chain_lower_map:
   assumes "approx_chain a"
@@ -475,7 +475,7 @@
     by (fast intro!: approx_chain_lower_map)
 qed
 
-subsection {* Join *}
+subsection \<open>Join\<close>
 
 definition
   lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Map_Functions.thy
--- a/src/HOL/HOLCF/Map_Functions.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Map_Functions.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Map functions for various types *}
+section \<open>Map functions for various types\<close>
 
 theory Map_Functions
 imports Deflation
 begin
 
-subsection {* Map operator for continuous function space *}
+subsection \<open>Map operator for continuous function space\<close>
 
 default_sort cpo
 
@@ -105,7 +105,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
-text {* Finite deflations are compact elements of the function space *}
+text \<open>Finite deflations are compact elements of the function space\<close>
 
 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
 apply (frule finite_deflation_imp_deflation)
@@ -115,7 +115,7 @@
 apply (simp only: finite_deflation_cfun_map)
 done
 
-subsection {* Map operator for product type *}
+subsection \<open>Map operator for product type\<close>
 
 definition
   prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
@@ -172,7 +172,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Map function for lifted cpo *}
+subsection \<open>Map function for lifted cpo\<close>
 
 definition
   u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
@@ -218,7 +218,7 @@
     by (rule finite_subset, simp add: d.finite_fixes)
 qed
 
-subsection {* Map function for strict products *}
+subsection \<open>Map function for strict products\<close>
 
 default_sort pcpo
 
@@ -299,7 +299,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Map function for strict sums *}
+subsection \<open>Map function for strict sums\<close>
 
 definition
   ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
@@ -383,7 +383,7 @@
     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
 qed
 
-subsection {* Map operator for strict function space *}
+subsection \<open>Map operator for strict function space\<close>
 
 definition
   sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
@@ -461,7 +461,7 @@
   then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
     unfolding sfun_map_def sfun_eq_iff
     by (simp add: strictify_cancel
-         deflation_strict `deflation d1` `deflation d2`)
+         deflation_strict \<open>deflation d1\<close> \<open>deflation d2\<close>)
 qed
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/One.thy
--- a/src/HOL/HOLCF/One.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/One.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Oscar Slotosch
 *)
 
-section {* The unit domain *}
+section \<open>The unit domain\<close>
 
 theory One
 imports Lift
@@ -17,7 +17,7 @@
 definition ONE :: "one"
   where "ONE == Def ()"
 
-text {* Exhaustion and Elimination for type @{typ one} *}
+text \<open>Exhaustion and Elimination for type @{typ one}\<close>
 
 lemma Exh_one: "t = \<bottom> \<or> t = ONE"
 unfolding ONE_def by (induct t) simp_all
@@ -50,7 +50,7 @@
 lemma compact_ONE: "compact ONE"
 by (rule compact_chfin)
 
-text {* Case analysis function for type @{typ one} *}
+text \<open>Case analysis function for type @{typ one}\<close>
 
 definition
   one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,21 +2,21 @@
     Author:     Franz Regensburger
 *)
 
-section {* Classes cpo and pcpo *}
+section \<open>Classes cpo and pcpo\<close>
 
 theory Pcpo
 imports Porder
 begin
 
-subsection {* Complete partial orders *}
+subsection \<open>Complete partial orders\<close>
 
-text {* The class cpo of chain complete partial orders *}
+text \<open>The class cpo of chain complete partial orders\<close>
 
 class cpo = po +
   assumes cpo: "chain S \<Longrightarrow> \<exists>x. range S <<| x"
 begin
 
-text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
+text \<open>in cpo's everthing equal to THE lub has lub properties for every chain\<close>
 
 lemma cpo_lubI: "chain S \<Longrightarrow> range S <<| (\<Squnion>i. S i)"
   by (fast dest: cpo elim: is_lub_lub)
@@ -24,7 +24,7 @@
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = l\<rbrakk> \<Longrightarrow> range S <<| l"
   by (blast dest: cpo intro: is_lub_lub)
 
-text {* Properties of the lub *}
+text \<open>Properties of the lub\<close>
 
 lemma is_ub_thelub: "chain S \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
   by (blast dest: cpo intro: is_lub_lub [THEN is_lub_rangeD1])
@@ -78,14 +78,14 @@
 apply (force elim!: is_ub_thelub)
 done
 
-text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
+text \<open>the \<open>\<sqsubseteq>\<close> relation between two chains is preserved by their lubs\<close>
 
 lemma lub_mono:
   "\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
 by (fast elim: lub_below below_lub)
 
-text {* the = relation between two chains is preserved by their lubs *}
+text \<open>the = relation between two chains is preserved by their lubs\<close>
 
 lemma lub_eq:
   "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
@@ -135,9 +135,9 @@
 
 end
 
-subsection {* Pointed cpos *}
+subsection \<open>Pointed cpos\<close>
 
-text {* The class pcpo of pointed cpos *}
+text \<open>The class pcpo of pointed cpos\<close>
 
 class pcpo = cpo +
   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
@@ -157,22 +157,22 @@
 
 end
 
-text {* Old "UU" syntax: *}
+text \<open>Old "UU" syntax:\<close>
 
 syntax UU :: logic
 
 translations "UU" => "CONST bottom"
 
-text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
+text \<open>Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}.\<close>
 
-setup {*
+setup \<open>
   Reorient_Proc.add
     (fn Const(@{const_name bottom}, _) => true | _ => false)
-*}
+\<close>
 
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
 
-text {* useful lemmas about @{term \<bottom>} *}
+text \<open>useful lemmas about @{term \<bottom>}\<close>
 
 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
 by (simp add: po_eq_conv)
@@ -186,9 +186,9 @@
 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)"
 by (simp only: eq_bottom_iff lub_below_iff)
 
-subsection {* Chain-finite and flat cpos *}
+subsection \<open>Chain-finite and flat cpos\<close>
 
-text {* further useful classes for HOLCF domains *}
+text \<open>further useful classes for HOLCF domains\<close>
 
 class chfin = po +
   assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
@@ -230,7 +230,7 @@
 
 end
 
-subsection {* Discrete cpos *}
+subsection \<open>Discrete cpos\<close>
 
 class discrete_cpo = below +
   assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
@@ -239,7 +239,7 @@
 subclass po
 proof qed simp_all
 
-text {* In a discrete cpo, every chain is constant *}
+text \<open>In a discrete cpo, every chain is constant\<close>
 
 lemma discrete_chain_const:
   assumes S: "chain S"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Plain_HOLCF.thy
--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,15 +2,15 @@
     Author:     Brian Huffman
 *)
 
-section {* Plain HOLCF *}
+section \<open>Plain HOLCF\<close>
 
 theory Plain_HOLCF
 imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
 begin
 
-text {*
+text \<open>
   Basic HOLCF concepts and types; does not include definition packages.
-*}
+\<close>
 
 hide_const (open) Filter.principal
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Porder.thy
--- a/src/HOL/HOLCF/Porder.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Porder.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger and Brian Huffman
 *)
 
-section {* Partial orders *}
+section \<open>Partial orders\<close>
 
 theory Porder
 imports Main
@@ -11,7 +11,7 @@
 declare [[typedef_overloaded]]
 
 
-subsection {* Type class for partial orders *}
+subsection \<open>Type class for partial orders\<close>
 
 class below =
   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -70,7 +70,7 @@
 context po
 begin
 
-subsection {* Upper bounds *}
+subsection \<open>Upper bounds\<close>
 
 definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where
   "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
@@ -102,7 +102,7 @@
 lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
   unfolding is_ub_def by (fast intro: below_trans)
 
-subsection {* Least upper bounds *}
+subsection \<open>Least upper bounds\<close>
 
 definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where
   "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
@@ -131,7 +131,7 @@
 notation (ASCII)
   Lub  (binder "LUB " 10)
 
-text {* access to some definition as inference rule *}
+text \<open>access to some definition as inference rule\<close>
 
 lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
   unfolding is_lub_def by fast
@@ -145,12 +145,12 @@
 lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u"
   unfolding is_lub_def is_ub_def by (metis below_trans)
 
-text {* lubs are unique *}
+text \<open>lubs are unique\<close>
 
 lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
   unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
 
-text {* technical lemmas about @{term lub} and @{term is_lub} *}
+text \<open>technical lemmas about @{term lub} and @{term is_lub}\<close>
 
 lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
   unfolding lub_def by (rule theI [OF _ is_lub_unique])
@@ -176,10 +176,10 @@
 lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
   by (rule is_lub_maximal [THEN lub_eqI])
 
-subsection {* Countable chains *}
+subsection \<open>Countable chains\<close>
 
 definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
-  -- {* Here we use countable chains and I prefer to code them as functions! *}
+  \<comment> \<open>Here we use countable chains and I prefer to code them as functions!\<close>
   "chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
 
 lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
@@ -188,7 +188,7 @@
 lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)"
   unfolding chain_def by fast
 
-text {* chains are monotone functions *}
+text \<open>chains are monotone functions\<close>
 
 lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
   by (erule less_Suc_induct, erule chainE, erule below_trans)
@@ -199,7 +199,7 @@
 lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
   by (rule chainI, simp, erule chainE)
 
-text {* technical lemmas about (least) upper bounds of chains *}
+text \<open>technical lemmas about (least) upper bounds of chains\<close>
 
 lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
   by (rule is_lubD1 [THEN ub_rangeD])
@@ -220,7 +220,7 @@
   "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
   by (simp add: is_lub_def is_ub_range_shift)
 
-text {* the lub of a constant chain is the constant *}
+text \<open>the lub of a constant chain is the constant\<close>
 
 lemma chain_const [simp]: "chain (\<lambda>i. c)"
   by (simp add: chainI)
@@ -231,16 +231,16 @@
 lemma lub_const [simp]: "(\<Squnion>i. c) = c"
   by (rule is_lub_const [THEN lub_eqI])
 
-subsection {* Finite chains *}
+subsection \<open>Finite chains\<close>
 
 definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where
-  -- {* finite chains, needed for monotony of continuous functions *}
+  \<comment> \<open>finite chains, needed for monotony of continuous functions\<close>
   "max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
 
 definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
 
-text {* results about finite chains *}
+text \<open>results about finite chains\<close>
 
 lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y"
   unfolding max_in_chain_def by fast
@@ -336,7 +336,7 @@
 apply simp
 done
 
-text {* the maximal element in a chain is its lub *}
+text \<open>the maximal element in a chain is its lub\<close>
 
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
   by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Powerdomains.thy
--- a/src/HOL/HOLCF/Powerdomains.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Powerdomains.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Powerdomains *}
+section \<open>Powerdomains\<close>
 
 theory Powerdomains
 imports ConvexPD Domain
 begin
 
-subsection {* Universal domain embeddings *}
+subsection \<open>Universal domain embeddings\<close>
 
 definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
 definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
@@ -31,7 +31,7 @@
   unfolding convex_emb_def convex_prj_def
   by (simp add: ep_pair_udom approx_chain_convex_map)
 
-subsection {* Deflation combinators *}
+subsection \<open>Deflation combinators\<close>
 
 definition upper_defl :: "udom defl \<rightarrow> udom defl"
   where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
@@ -57,7 +57,7 @@
 using ep_pair_convex finite_deflation_convex_map
 unfolding convex_defl_def by (rule cast_defl_fun1)
 
-subsection {* Domain class instances *}
+subsection \<open>Domain class instances\<close>
 
 instantiation upper_pd :: ("domain") "domain"
 begin
@@ -167,7 +167,7 @@
 lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
 by (rule defl_convex_pd_def)
 
-subsection {* Isomorphic deflations *}
+subsection \<open>Isomorphic deflations\<close>
 
 lemma isodefl_upper:
   "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
@@ -193,7 +193,7 @@
 apply (simp add: convex_map_map)
 done
 
-subsection {* Domain package setup for powerdomains *}
+subsection \<open>Domain package setup for powerdomains\<close>
 
 lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
 lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
@@ -202,11 +202,11 @@
 lemmas [domain_deflation] =
   deflation_upper_map deflation_lower_map deflation_convex_map
 
-setup {*
+setup \<open>
   fold Domain_Take_Proofs.add_rec_type
     [(@{type_name "upper_pd"}, [true]),
      (@{type_name "lower_pd"}, [true]),
      (@{type_name "convex_pd"}, [true])]
-*}
+\<close>
 
 end
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Product_Cpo.thy
--- a/src/HOL/HOLCF/Product_Cpo.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Product_Cpo.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-section {* The cpo of cartesian products *}
+section \<open>The cpo of cartesian products\<close>
 
 theory Product_Cpo
 imports Adm
@@ -10,7 +10,7 @@
 
 default_sort cpo
 
-subsection {* Unit type is a pcpo *}
+subsection \<open>Unit type is a pcpo\<close>
 
 instantiation unit :: discrete_cpo
 begin
@@ -27,7 +27,7 @@
 by intro_classes simp
 
 
-subsection {* Product type is a partial order *}
+subsection \<open>Product type is a partial order\<close>
 
 instantiation prod :: (below, below) below
 begin
@@ -55,7 +55,7 @@
     by (fast intro: below_trans)
 qed
 
-subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
+subsection \<open>Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
 
 lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
 unfolding below_prod_def by simp
@@ -63,7 +63,7 @@
 lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
 unfolding below_prod_def by simp
 
-text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
+text \<open>Pair \<open>(_,_)\<close>  is monotone in both arguments\<close>
 
 lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
 by (simp add: monofun_def)
@@ -79,7 +79,7 @@
   "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
 by (rule chainI, simp add: chainE)
 
-text {* @{term fst} and @{term snd} are monotone *}
+text \<open>@{term fst} and @{term snd} are monotone\<close>
 
 lemma fst_monofun: "x \<sqsubseteq> y \<Longrightarrow> fst x \<sqsubseteq> fst y"
 unfolding below_prod_def by simp
@@ -102,12 +102,12 @@
   obtains A B
   where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
 proof
-  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
-  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
+  from \<open>chain Y\<close> show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
+  from \<open>chain Y\<close> show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
   show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
 qed
 
-subsection {* Product type is a cpo *}
+subsection \<open>Product type is a cpo\<close>
 
 lemma is_lub_Pair:
   "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
@@ -146,7 +146,7 @@
     by simp
 qed
 
-subsection {* Product type is pointed *}
+subsection \<open>Product type is pointed\<close>
 
 lemma minimal_prod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
 by (simp add: below_prod_def)
@@ -172,7 +172,7 @@
 lemma split_strict [simp]: "case_prod f \<bottom> = f \<bottom> \<bottom>"
 unfolding split_def by simp
 
-subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
+subsection \<open>Continuity of \emph{Pair}, \emph{fst}, \emph{snd}\<close>
 
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
 apply (rule contI)
@@ -252,22 +252,22 @@
   shows "cont (\<lambda>x. case_prod (f x) (g x))"
 using assms by (simp add: cont2cont_case_prod prod_cont_iff)
 
-text {* The simple version (due to Joachim Breitner) is needed if
-  either element type of the pair is not a cpo. *}
+text \<open>The simple version (due to Joachim Breitner) is needed if
+  either element type of the pair is not a cpo.\<close>
 
 lemma cont2cont_split_simple [simp, cont2cont]:
  assumes "\<And>a b. cont (\<lambda>x. f x a b)"
  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
 using assms by (cases p) auto
 
-text {* Admissibility of predicates on product types. *}
+text \<open>Admissibility of predicates on product types.\<close>
 
 lemma adm_case_prod [simp]:
   assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
   shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
 unfolding case_prod_beta using assms .
 
-subsection {* Compactness and chain-finiteness *}
+subsection \<open>Compactness and chain-finiteness\<close>
 
 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
 unfolding below_prod_def by simp
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Representable.thy
--- a/src/HOL/HOLCF/Representable.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Representable.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Representable domains *}
+section \<open>Representable domains\<close>
 
 theory Representable
 imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
@@ -10,9 +10,9 @@
 
 default_sort cpo
 
-subsection {* Class of representable domains *}
+subsection \<open>Class of representable domains\<close>
 
-text {*
+text \<open>
   We define a ``domain'' as a pcpo that is isomorphic to some
   algebraic deflation over the universal domain; this is equivalent
   to being omega-bifinite.
@@ -20,7 +20,7 @@
   A predomain is a cpo that, when lifted, becomes a domain.
   Predomains are represented by deflations over a lifted universal
   domain type.
-*}
+\<close>
 
 class predomain_syn = cpo +
   fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
@@ -63,16 +63,16 @@
     by (simp add: cast_liftdefl_of cast_DEFL u_map_oo)
 qed
 
-text {*
+text \<open>
   Constants @{const liftemb} and @{const liftprj} imply class predomain.
-*}
+\<close>
 
-setup {*
+setup \<open>
   fold Sign.add_const_constraint
   [(@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
    (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}),
    (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})]
-*}
+\<close>
 
 interpretation predomain: pcpo_ep_pair liftemb liftprj
   unfolding pcpo_ep_pair_def by (rule predomain_ep)
@@ -86,7 +86,7 @@
 lemmas emb_strict = domain.e_strict
 lemmas prj_strict = domain.p_strict
 
-subsection {* Domains are bifinite *}
+subsection \<open>Domains are bifinite\<close>
 
 lemma approx_chain_ep_cast:
   assumes ep: "ep_pair (e::'a::pcpo \<rightarrow> 'b::bifinite) (p::'b \<rightarrow> 'a)"
@@ -124,7 +124,7 @@
 instance predomain \<subseteq> profinite
 by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
 
-subsection {* Universal domain ep-pairs *}
+subsection \<open>Universal domain ep-pairs\<close>
 
 definition "u_emb = udom_emb (\<lambda>i. u_map\<cdot>(udom_approx i))"
 definition "u_prj = udom_prj (\<lambda>i. u_map\<cdot>(udom_approx i))"
@@ -161,7 +161,7 @@
   unfolding sfun_emb_def sfun_prj_def
   by (simp add: ep_pair_udom approx_chain_sfun_map)
 
-subsection {* Type combinators *}
+subsection \<open>Type combinators\<close>
 
 definition u_defl :: "udom defl \<rightarrow> udom defl"
   where "u_defl = defl_fun1 u_emb u_prj u_map"
@@ -207,7 +207,7 @@
 using ep_pair_sfun finite_deflation_sfun_map
 unfolding sfun_defl_def by (rule cast_defl_fun2)
 
-text {* Special deflation combinator for unpointed types. *}
+text \<open>Special deflation combinator for unpointed types.\<close>
 
 definition u_liftdefl :: "udom u defl \<rightarrow> udom defl"
   where "u_liftdefl = defl_fun1 u_emb u_prj ID"
@@ -221,9 +221,9 @@
 by (rule cast_eq_imp_eq)
    (simp add: cast_u_liftdefl cast_liftdefl_of cast_u_defl)
 
-subsection {* Class instance proofs *}
+subsection \<open>Class instance proofs\<close>
 
-subsubsection {* Universal domain *}
+subsubsection \<open>Universal domain\<close>
 
 instantiation udom :: "domain"
 begin
@@ -265,7 +265,7 @@
 
 end
 
-subsubsection {* Lifted cpo *}
+subsubsection \<open>Lifted cpo\<close>
 
 instantiation u :: (predomain) "domain"
 begin
@@ -302,7 +302,7 @@
 lemma DEFL_u: "DEFL('a::predomain u) = u_liftdefl\<cdot>LIFTDEFL('a)"
 by (rule defl_u_def)
 
-subsubsection {* Strict function space *}
+subsubsection \<open>Strict function space\<close>
 
 instantiation sfun :: ("domain", "domain") "domain"
 begin
@@ -340,7 +340,7 @@
   "DEFL('a::domain \<rightarrow>! 'b::domain) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sfun_def)
 
-subsubsection {* Continuous function space *}
+subsubsection \<open>Continuous function space\<close>
 
 instantiation cfun :: (predomain, "domain") "domain"
 begin
@@ -380,7 +380,7 @@
   "DEFL('a::predomain \<rightarrow> 'b::domain) = DEFL('a u \<rightarrow>! 'b)"
 by (rule defl_cfun_def)
 
-subsubsection {* Strict product *}
+subsubsection \<open>Strict product\<close>
 
 instantiation sprod :: ("domain", "domain") "domain"
 begin
@@ -418,7 +418,7 @@
   "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sprod_def)
 
-subsubsection {* Cartesian product *}
+subsubsection \<open>Cartesian product\<close>
 
 definition prod_liftdefl :: "udom u defl \<rightarrow> udom u defl \<rightarrow> udom u defl"
   where "prod_liftdefl = defl_fun2 (u_map\<cdot>prod_emb oo decode_prod_u)
@@ -506,7 +506,7 @@
     prod_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
 by (rule liftdefl_prod_def)
 
-subsubsection {* Unit type *}
+subsubsection \<open>Unit type\<close>
 
 instantiation unit :: "domain"
 begin
@@ -539,7 +539,7 @@
 
 end
 
-subsubsection {* Discrete cpo *}
+subsubsection \<open>Discrete cpo\<close>
 
 instantiation discr :: (countable) predomain
 begin
@@ -584,7 +584,7 @@
 
 end
 
-subsubsection {* Strict sum *}
+subsubsection \<open>Strict sum\<close>
 
 instantiation ssum :: ("domain", "domain") "domain"
 begin
@@ -622,7 +622,7 @@
   "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_ssum_def)
 
-subsubsection {* Lifted HOL type *}
+subsubsection \<open>Lifted HOL type\<close>
 
 instantiation lift :: (countable) "domain"
 begin
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Sfun.thy
--- a/src/HOL/HOLCF/Sfun.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The Strict Function Type *}
+section \<open>The Strict Function Type\<close>
 
 theory Sfun
 imports Cfun
@@ -15,7 +15,7 @@
 type_notation (ASCII)
   sfun  (infixr "->!" 0)
 
-text {* TODO: Define nice syntax for abstraction, application. *}
+text \<open>TODO: Define nice syntax for abstraction, application.\<close>
 
 definition
   sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The type of strict products *}
+section \<open>The type of strict products\<close>
 
 theory Sprod
 imports Cfun
@@ -11,7 +11,7 @@
 
 default_sort pcpo
 
-subsection {* Definition of strict product type *}
+subsection \<open>Definition of strict product type\<close>
 
 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
@@ -25,7 +25,7 @@
   sprod  (infixr "**" 20)
 
 
-subsection {* Definitions of constants *}
+subsection \<open>Definitions of constants\<close>
 
 definition
   sfst :: "('a ** 'b) \<rightarrow> 'a" where
@@ -53,7 +53,7 @@
 translations
   "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
 
-subsection {* Case analysis *}
+subsection \<open>Case analysis\<close>
 
 lemma spair_sprod: "(seq\<cdot>b\<cdot>a, seq\<cdot>a\<cdot>b) \<in> sprod"
 by (simp add: sprod_def seq_conv_if)
@@ -74,7 +74,7 @@
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
-subsection {* Properties of \emph{spair} *}
+subsection \<open>Properties of \emph{spair}\<close>
 
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
 by (simp add: Rep_sprod_simps)
@@ -124,7 +124,7 @@
 lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
 by (cases p, simp only: inst_sprod_pcpo2, simp)
 
-subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
+subsection \<open>Properties of \emph{sfst} and \emph{ssnd}\<close>
 
 lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
 by (simp add: sfst_def cont_Rep_sprod Rep_sprod_strict)
@@ -169,7 +169,7 @@
 apply (simp add: below_sprod)
 done
 
-subsection {* Compactness *}
+subsection \<open>Compactness\<close>
 
 lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
 by (rule compactI, simp add: sfst_below_iff)
@@ -189,7 +189,7 @@
 apply simp
 done
 
-subsection {* Properties of \emph{ssplit} *}
+subsection \<open>Properties of \emph{ssplit}\<close>
 
 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: ssplit_def)
@@ -200,7 +200,7 @@
 lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
 by (cases z, simp_all)
 
-subsection {* Strict product preserves flatness *}
+subsection \<open>Strict product preserves flatness\<close>
 
 instance sprod :: (flat, flat) flat
 proof
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -3,7 +3,7 @@
     Author:     Brian Huffman
 *)
 
-section {* The type of strict sums *}
+section \<open>The type of strict sums\<close>
 
 theory Ssum
 imports Tr
@@ -11,7 +11,7 @@
 
 default_sort pcpo
 
-subsection {* Definition of strict sum type *}
+subsection \<open>Definition of strict sum type\<close>
 
 definition
   "ssum =
@@ -29,7 +29,7 @@
   ssum  (infixr "++" 10)
 
 
-subsection {* Definitions of constructors *}
+subsection \<open>Definitions of constructors\<close>
 
 definition
   sinl :: "'a \<rightarrow> ('a ++ 'b)" where
@@ -56,9 +56,9 @@
   prod_eq_iff below_prod_def
   Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
 
-subsection {* Properties of \emph{sinl} and \emph{sinr} *}
+subsection \<open>Properties of \emph{sinl} and \emph{sinr}\<close>
 
-text {* Ordering *}
+text \<open>Ordering\<close>
 
 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: Rep_ssum_simps seq_conv_if)
@@ -72,7 +72,7 @@
 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
 by (simp add: Rep_ssum_simps seq_conv_if)
 
-text {* Equality *}
+text \<open>Equality\<close>
 
 lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
 by (simp add: po_eq_conv)
@@ -92,7 +92,7 @@
 lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
 by (rule sinr_eq [THEN iffD1])
 
-text {* Strictness *}
+text \<open>Strictness\<close>
 
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
 by (simp add: Rep_ssum_simps)
@@ -112,7 +112,7 @@
 lemma sinr_defined: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
 by simp
 
-text {* Compactness *}
+text \<open>Compactness\<close>
 
 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
 by (rule compact_ssum, simp add: Rep_ssum_sinl)
@@ -134,7 +134,7 @@
 lemma compact_sinr_iff [simp]: "compact (sinr\<cdot>x) = compact x"
 by (safe elim!: compact_sinr compact_sinrD)
 
-subsection {* Case analysis *}
+subsection \<open>Case analysis\<close>
 
 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
   obtains "p = \<bottom>"
@@ -158,7 +158,7 @@
 lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
 by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
 
-subsection {* Case analysis combinator *}
+subsection \<open>Case analysis combinator\<close>
 
 definition
   sscase :: "('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a ++ 'b) \<rightarrow> 'c" where
@@ -188,7 +188,7 @@
 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
 
-subsection {* Strict sum preserves flatness *}
+subsection \<open>Strict sum preserves flatness\<close>
 
 instance ssum :: (flat, flat) flat
 apply (intro_classes, clarify)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Tr.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Franz Regensburger
 *)
 
-section {* The type of lifted booleans *}
+section \<open>The type of lifted booleans\<close>
 
 theory Tr
 imports Lift
 begin
 
-subsection {* Type definition and constructors *}
+subsection \<open>Type definition and constructors\<close>
 
 type_synonym
   tr = "bool lift"
@@ -24,7 +24,7 @@
   FF :: "tr" where
   "FF = Def False"
 
-text {* Exhaustion and Elimination for type @{typ tr} *}
+text \<open>Exhaustion and Elimination for type @{typ tr}\<close>
 
 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
 unfolding FF_def TT_def by (induct t) auto
@@ -37,7 +37,7 @@
   "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
 by (cases x) simp_all
 
-text {* distinctness for type @{typ tr} *}
+text \<open>distinctness for type @{typ tr}\<close>
 
 lemma dist_below_tr [simp]:
   "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
@@ -60,7 +60,7 @@
 by (induct x) simp_all
 
 
-subsection {* Case analysis *}
+subsection \<open>Case analysis\<close>
 
 default_sort pcpo
 
@@ -83,7 +83,7 @@
 by (simp_all add: tr_case_def TT_def FF_def)
 
 
-subsection {* Boolean connectives *}
+subsection \<open>Boolean connectives\<close>
 
 definition
   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
@@ -107,11 +107,11 @@
   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
   "If2 Q x y = (If Q then x else y)"
 
-text {* tactic for tr-thms with case split *}
+text \<open>tactic for tr-thms with case split\<close>
 
 lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
 
-text {* lemmas about andalso, orelse, neg and if *}
+text \<open>lemmas about andalso, orelse, neg and if\<close>
 
 lemma andalso_thms [simp]:
   "(TT andalso y) = y"
@@ -141,7 +141,7 @@
   "neg\<cdot>\<bottom> = \<bottom>"
 by (simp_all add: neg_def TT_def FF_def)
 
-text {* split-tac for If via If2 because the constant has to be a constant *}
+text \<open>split-tac for If via If2 because the constant has to be a constant\<close>
 
 lemma split_If2:
   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
@@ -151,11 +151,11 @@
 done
 
 (* FIXME unused!? *)
-ML {*
+ML \<open>
 fun split_If_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
     THEN' (split_tac ctxt [@{thm split_If2}])
-*}
+\<close>
 
 subsection "Rewriting of HOLCF operations to HOL functions"
 
@@ -189,7 +189,7 @@
 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
 done
 
-subsection {* Compactness *}
+subsection \<open>Compactness\<close>
 
 lemma compact_TT: "compact TT"
 by (rule compact_chfin)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Tutorial/Domain_ex.thy
--- a/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Tutorial/Domain_ex.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,43 +2,43 @@
     Author:     Brian Huffman
 *)
 
-section {* Domain package examples *}
+section \<open>Domain package examples\<close>
 
 theory Domain_ex
 imports HOLCF
 begin
 
-text {* Domain constructors are strict by default. *}
+text \<open>Domain constructors are strict by default.\<close>
 
 domain d1 = d1a | d1b "d1" "d1"
 
 lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp
 
-text {* Constructors can be made lazy using the @{text "lazy"} keyword. *}
+text \<open>Constructors can be made lazy using the \<open>lazy\<close> keyword.\<close>
 
 domain d2 = d2a | d2b (lazy "d2")
 
 lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp
 
-text {* Strict and lazy arguments may be mixed arbitrarily. *}
+text \<open>Strict and lazy arguments may be mixed arbitrarily.\<close>
 
 domain d3 = d3a | d3b (lazy "d2") "d2"
 
 lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp
 
-text {* Selectors can be used with strict or lazy constructor arguments. *}
+text \<open>Selectors can be used with strict or lazy constructor arguments.\<close>
 
 domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2")
 
 lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp
 
-text {* Mixfix declarations can be given for data constructors. *}
+text \<open>Mixfix declarations can be given for data constructors.\<close>
 
 domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70)
 
 lemma "d5a \<noteq> x :#: y :#: z" by simp
 
-text {* Mixfix declarations can also be given for type constructors. *}
+text \<open>Mixfix declarations can also be given for type constructors.\<close>
 
 domain ('a, 'b) lazypair (infixl ":*:" 25) =
   lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75)
@@ -46,34 +46,34 @@
 lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p"
 by (rule allI, case_tac p, simp_all)
 
-text {* Non-recursive constructor arguments can have arbitrary types. *}
+text \<open>Non-recursive constructor arguments can have arbitrary types.\<close>
 
 domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)")
 
-text {*
+text \<open>
   Indirect recusion is allowed for sums, products, lifting, and the
   continuous function space.  However, the domain package does not
   generate an induction rule in terms of the constructors.
-*}
+\<close>
 
 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
-  -- "Indirect recursion detected, skipping proofs of (co)induction rules"
+  \<comment> "Indirect recursion detected, skipping proofs of (co)induction rules"
 
-text {* Note that @{text d7.induct} is absent. *}
+text \<open>Note that \<open>d7.induct\<close> is absent.\<close>
 
-text {*
+text \<open>
   Indirect recursion is also allowed using previously-defined datatypes.
-*}
+\<close>
 
 domain 'a slist = SNil | SCons 'a "'a slist"
 
 domain 'a stree = STip | SBranch "'a stree slist"
 
-text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *}
+text \<open>Mutually-recursive datatypes can be defined using the \<open>and\<close> keyword.\<close>
 
 domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8")
 
-text {* Non-regular recursion is not allowed. *}
+text \<open>Non-regular recursion is not allowed.\<close>
 (*
 domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist"
   -- "illegal direct recursion with different arguments"
@@ -81,54 +81,54 @@
   -- "illegal direct recursion with different arguments"
 *)
 
-text {*
+text \<open>
   Mutually-recursive datatypes must have all the same type arguments,
   not necessarily in the same order.
-*}
+\<close>
 
 domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2"
    and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1"
 
-text {* Induction rules for flat datatypes have no admissibility side-condition. *}
+text \<open>Induction rules for flat datatypes have no admissibility side-condition.\<close>
 
 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree"
 
 lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
-by (rule flattree.induct) -- "no admissibility requirement"
+by (rule flattree.induct) \<comment> "no admissibility requirement"
 
-text {* Trivial datatypes will produce a warning message. *}
+text \<open>Trivial datatypes will produce a warning message.\<close>
 
 domain triv = Triv triv triv
-  -- "domain @{text Domain_ex.triv} is empty!"
+  \<comment> "domain \<open>Domain_ex.triv\<close> is empty!"
 
 lemma "(x::triv) = \<bottom>" by (induct x, simp_all)
 
-text {* Lazy constructor arguments may have unpointed types. *}
+text \<open>Lazy constructor arguments may have unpointed types.\<close>
 
 domain natlist = nnil | ncons (lazy "nat discr") natlist
 
-text {* Class constraints may be given for type parameters on the LHS. *}
+text \<open>Class constraints may be given for type parameters on the LHS.\<close>
 
 domain ('a::predomain) box = Box (lazy 'a)
 
 domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream"
 
 
-subsection {* Generated constants and theorems *}
+subsection \<open>Generated constants and theorems\<close>
 
 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree")
 
 lemmas tree_abs_bottom_iff =
   iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]]
 
-text {* Rules about ismorphism *}
+text \<open>Rules about ismorphism\<close>
 term tree_rep
 term tree_abs
 thm tree.rep_iso
 thm tree.abs_iso
 thm tree.iso_rews
 
-text {* Rules about constructors *}
+text \<open>Rules about constructors\<close>
 term Leaf
 term Node
 thm Leaf_def Node_def
@@ -141,27 +141,27 @@
 thm tree.inverts
 thm tree.injects
 
-text {* Rules about case combinator *}
+text \<open>Rules about case combinator\<close>
 term tree_case
 thm tree.tree_case_def
 thm tree.case_rews
 
-text {* Rules about selectors *}
+text \<open>Rules about selectors\<close>
 term left
 term right
 thm tree.sel_rews
 
-text {* Rules about discriminators *}
+text \<open>Rules about discriminators\<close>
 term is_Leaf
 term is_Node
 thm tree.dis_rews
 
-text {* Rules about monadic pattern match combinators *}
+text \<open>Rules about monadic pattern match combinators\<close>
 term match_Leaf
 term match_Node
 thm tree.match_rews
 
-text {* Rules about take function *}
+text \<open>Rules about take function\<close>
 term tree_take
 thm tree.take_def
 thm tree.take_0
@@ -176,23 +176,23 @@
 thm tree.reach
 thm tree.finite_induct
 
-text {* Rules about finiteness predicate *}
+text \<open>Rules about finiteness predicate\<close>
 term tree_finite
 thm tree.finite_def
 thm tree.finite (* only generated for flat datatypes *)
 
-text {* Rules about bisimulation predicate *}
+text \<open>Rules about bisimulation predicate\<close>
 term tree_bisim
 thm tree.bisim_def
 thm tree.coinduct
 
-text {* Induction rule *}
+text \<open>Induction rule\<close>
 thm tree.induct
 
 
-subsection {* Known bugs *}
+subsection \<open>Known bugs\<close>
 
-text {* Declaring a mixfix with spaces causes some strange parse errors. *}
+text \<open>Declaring a mixfix with spaces causes some strange parse errors.\<close>
 (*
 domain xx = xx ("x y")
   -- "Inner syntax error: unexpected end of input"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Tutorial/Fixrec_ex.thy
--- a/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Tutorial/Fixrec_ex.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,50 +2,50 @@
     Author:     Brian Huffman
 *)
 
-section {* Fixrec package examples *}
+section \<open>Fixrec package examples\<close>
 
 theory Fixrec_ex
 imports HOLCF
 begin
 
-subsection {* Basic @{text fixrec} examples *}
+subsection \<open>Basic \<open>fixrec\<close> examples\<close>
 
-text {*
+text \<open>
   Fixrec patterns can mention any constructor defined by the domain
   package, as well as any of the following built-in constructors:
   Pair, spair, sinl, sinr, up, ONE, TT, FF.
-*}
+\<close>
 
-text {* Typical usage is with lazy constructors. *}
+text \<open>Typical usage is with lazy constructors.\<close>
 
 fixrec down :: "'a u \<rightarrow> 'a"
 where "down\<cdot>(up\<cdot>x) = x"
 
-text {* With strict constructors, rewrite rules may require side conditions. *}
+text \<open>With strict constructors, rewrite rules may require side conditions.\<close>
 
 fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
 where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
 
-text {* Lifting can turn a strict constructor into a lazy one. *}
+text \<open>Lifting can turn a strict constructor into a lazy one.\<close>
 
 fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
 where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
 
-text {* Fixrec also works with the HOL pair constructor. *}
+text \<open>Fixrec also works with the HOL pair constructor.\<close>
 
 fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b"
 where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)"
 
 
-subsection {* Examples using @{text fixrec_simp} *}
+subsection \<open>Examples using \<open>fixrec_simp\<close>\<close>
 
-text {* A type of lazy lists. *}
+text \<open>A type of lazy lists.\<close>
 
 domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
 
-text {* A zip function for lazy lists. *}
+text \<open>A zip function for lazy lists.\<close>
 
-text {* Notice that the patterns are not exhaustive. *}
+text \<open>Notice that the patterns are not exhaustive.\<close>
 
 fixrec
   lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
@@ -53,8 +53,8 @@
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)"
 | "lzip\<cdot>lNil\<cdot>lNil = lNil"
 
-text {* @{text fixrec_simp} is useful for producing strictness theorems. *}
-text {* Note that pattern matching is done in left-to-right order. *}
+text \<open>\<open>fixrec_simp\<close> is useful for producing strictness theorems.\<close>
+text \<open>Note that pattern matching is done in left-to-right order.\<close>
 
 lemma lzip_stricts [simp]:
   "lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>"
@@ -62,7 +62,7 @@
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>"
 by fixrec_simp+
 
-text {* @{text fixrec_simp} can also produce rules for missing cases. *}
+text \<open>\<open>fixrec_simp\<close> can also produce rules for missing cases.\<close>
 
 lemma lzip_undefs [simp]:
   "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>"
@@ -70,14 +70,13 @@
 by fixrec_simp+
 
 
-subsection {* Pattern matching with bottoms *}
+subsection \<open>Pattern matching with bottoms\<close>
 
-text {*
-  As an alternative to using @{text fixrec_simp}, it is also possible
+text \<open>
+  As an alternative to using \<open>fixrec_simp\<close>, it is also possible
   to use bottom as a constructor pattern.  When using a bottom
-  pattern, the right-hand-side must also be bottom; otherwise, @{text
-  fixrec} will not be able to prove the equation.
-*}
+  pattern, the right-hand-side must also be bottom; otherwise, \<open>fixrec\<close> will not be able to prove the equation.
+\<close>
 
 fixrec
   from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b"
@@ -85,18 +84,18 @@
   "from_sinr_up\<cdot>\<bottom> = \<bottom>"
 | "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x"
 
-text {*
+text \<open>
   If the function is already strict in that argument, then the bottom
   pattern does not change the meaning of the function.  For example,
   in the definition of @{term from_sinr_up}, the first equation is
   actually redundant, and could have been proven separately by
-  @{text fixrec_simp}.
-*}
+  \<open>fixrec_simp\<close>.
+\<close>
 
-text {*
+text \<open>
   A bottom pattern can also be used to make a function strict in a
   certain argument, similar to a bang-pattern in Haskell.
-*}
+\<close>
 
 fixrec
   seq :: "'a \<rightarrow> 'b \<rightarrow> 'b"
@@ -105,15 +104,15 @@
 | "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y"
 
 
-subsection {* Skipping proofs of rewrite rules *}
+subsection \<open>Skipping proofs of rewrite rules\<close>
 
-text {* Another zip function for lazy lists. *}
+text \<open>Another zip function for lazy lists.\<close>
 
-text {*
+text \<open>
   Notice that this version has overlapping patterns.
   The second equation cannot be proved as a theorem
   because it only applies when the first pattern fails.
-*}
+\<close>
 
 fixrec
   lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
@@ -121,13 +120,13 @@
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)"
 | (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil"
 
-text {*
+text \<open>
   Usually fixrec tries to prove all equations as theorems.
   The "unchecked" option overrides this behavior, so fixrec
   does not attempt to prove that particular equation.
-*}
+\<close>
 
-text {* Simp rules can be generated later using @{text fixrec_simp}. *}
+text \<open>Simp rules can be generated later using \<open>fixrec_simp\<close>.\<close>
 
 lemma lzip2_simps [simp]:
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil"
@@ -141,17 +140,17 @@
 by fixrec_simp+
 
 
-subsection {* Mutual recursion with @{text fixrec} *}
+subsection \<open>Mutual recursion with \<open>fixrec\<close>\<close>
 
-text {* Tree and forest types. *}
+text \<open>Tree and forest types.\<close>
 
 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
 
-text {*
+text \<open>
   To define mutually recursive functions, give multiple type signatures
-  separated by the keyword @{text "and"}.
-*}
+  separated by the keyword \<open>and\<close>.
+\<close>
 
 fixrec
   map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
@@ -182,25 +181,25 @@
 *)
 
 
-subsection {* Looping simp rules *}
+subsection \<open>Looping simp rules\<close>
 
-text {*
+text \<open>
   The defining equations of a fixrec definition are declared as simp
   rules by default.  In some cases, especially for constants with no
   arguments or functions with variable patterns, the defining
   equations may cause the simplifier to loop.  In these cases it will
-  be necessary to use a @{text "[simp del]"} declaration.
-*}
+  be necessary to use a \<open>[simp del]\<close> declaration.
+\<close>
 
 fixrec
   repeat :: "'a \<rightarrow> 'a llist"
 where
   [simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)"
 
-text {*
+text \<open>
   We can derive other non-looping simp rules for @{const repeat} by
-  using the @{text subst} method with the @{text repeat.simps} rule.
-*}
+  using the \<open>subst\<close> method with the \<open>repeat.simps\<close> rule.
+\<close>
 
 lemma repeat_simps [simp]:
   "repeat\<cdot>x \<noteq> \<bottom>"
@@ -212,11 +211,11 @@
   "llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)"
 by (subst repeat.simps, simp)
 
-text {*
+text \<open>
   For mutually-recursive constants, looping might only occur if all
   equations are in the simpset at the same time.  In such cases it may
-  only be necessary to declare @{text "[simp del]"} on one equation.
-*}
+  only be necessary to declare \<open>[simp del]\<close> on one equation.
+\<close>
 
 fixrec
   inf_tree :: "'a tree" and inf_forest :: "'a forest"
@@ -225,7 +224,7 @@
 | "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)"
 
 
-subsection {* Using @{text fixrec} inside locales *}
+subsection \<open>Using \<open>fixrec\<close> inside locales\<close>
 
 locale test =
   fixes foo :: "'a \<rightarrow> 'a"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Tutorial/New_Domain.thy
--- a/src/HOL/HOLCF/Tutorial/New_Domain.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Tutorial/New_Domain.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,57 +2,57 @@
     Author:     Brian Huffman
 *)
 
-section {* Definitional domain package *}
+section \<open>Definitional domain package\<close>
 
 theory New_Domain
 imports HOLCF
 begin
 
-text {*
+text \<open>
   UPDATE: The definitional back-end is now the default mode of the domain
-  package. This file should be merged with @{text Domain_ex.thy}.
-*}
+  package. This file should be merged with \<open>Domain_ex.thy\<close>.
+\<close>
 
-text {*
-  Provided that @{text domain} is the default sort, the @{text new_domain}
+text \<open>
+  Provided that \<open>domain\<close> is the default sort, the \<open>new_domain\<close>
   package should work with any type definition supported by the old
   domain package.
-*}
+\<close>
 
 domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist")
 
-text {*
+text \<open>
   The difference is that the new domain package is completely
   definitional, and does not generate any axioms.  The following type
   and constant definitions are not produced by the old domain package.
-*}
+\<close>
 
 thm type_definition_llist
 thm llist_abs_def llist_rep_def
 
-text {*
+text \<open>
   The new domain package also adds support for indirect recursion with
   user-defined datatypes.  This definition of a tree datatype uses
   indirect recursion through the lazy list type constructor.
-*}
+\<close>
 
 domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist")
 
-text {*
+text \<open>
   For indirect-recursive definitions, the domain package is not able to
   generate a high-level induction rule.  (It produces a warning
   message instead.)  The low-level reach lemma (now proved as a
   theorem, no longer generated as an axiom) can be used to derive
   other induction rules.
-*}
+\<close>
 
 thm ltree.reach
 
-text {*
+text \<open>
   The definition of the take function uses map functions associated with
   each type constructor involved in the definition.  A map function
   for the lazy list type has been generated by the new domain package.
-*}
+\<close>
 
 thm ltree.take_rews
 thm llist_map_def
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,15 +2,15 @@
     Author:     Brian Huffman
 *)
 
-section {* A universal bifinite domain *}
+section \<open>A universal bifinite domain\<close>
 
 theory Universal
 imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
 begin
 
-subsection {* Basis for universal domain *}
+subsection \<open>Basis for universal domain\<close>
 
-subsubsection {* Basis datatype *}
+subsubsection \<open>Basis datatype\<close>
 
 type_synonym ubasis = nat
 
@@ -77,7 +77,7 @@
  apply (simp add: 2 node_gt1 node_gt2)
 done
 
-subsubsection {* Basis ordering *}
+subsubsection \<open>Basis ordering\<close>
 
 inductive
   ubasis_le :: "nat \<Rightarrow> nat \<Rightarrow> bool"
@@ -103,7 +103,7 @@
 apply (erule (1) ubasis_le_trans)
 done
 
-subsubsection {* Generic take function *}
+subsubsection \<open>Generic take function\<close>
 
 function
   ubasis_until :: "(ubasis \<Rightarrow> bool) \<Rightarrow> ubasis \<Rightarrow> ubasis"
@@ -195,7 +195,7 @@
 done
 
 
-subsection {* Defining the universal domain by ideal completion *}
+subsection \<open>Defining the universal domain by ideal completion\<close>
 
 typedef udom = "{S. udom.ideal S}"
 by (rule udom.ex_ideal)
@@ -230,7 +230,7 @@
 using udom_principal_def ubasis_countable
 by (rule udom.typedef_ideal_completion)
 
-text {* Universal domain is pointed *}
+text \<open>Universal domain is pointed\<close>
 
 lemma udom_minimal: "udom_principal 0 \<sqsubseteq> x"
 apply (induct x rule: udom.principal_induct)
@@ -244,7 +244,7 @@
 by (rule udom_minimal [THEN bottomI, symmetric])
 
 
-subsection {* Compact bases of domains *}
+subsection \<open>Compact bases of domains\<close>
 
 typedef 'a compact_basis = "{x::'a::pcpo. compact x}"
 by auto
@@ -285,16 +285,16 @@
 unfolding compact_le_def Rep_compact_bot by simp
 
 
-subsection {* Universality of \emph{udom} *}
+subsection \<open>Universality of \emph{udom}\<close>
 
-text {* We use a locale to parameterize the construction over a chain
-of approx functions on the type to be embedded. *}
+text \<open>We use a locale to parameterize the construction over a chain
+of approx functions on the type to be embedded.\<close>
 
 locale bifinite_approx_chain =
   approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
 begin
 
-subsubsection {* Choosing a maximal element from a finite set *}
+subsubsection \<open>Choosing a maximal element from a finite set\<close>
 
 lemma finite_has_maximal:
   fixes A :: "'a compact_basis set"
@@ -304,7 +304,7 @@
     show ?case by simp
 next
   case (insert a A)
-  from `\<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y`
+  from \<open>\<exists>x\<in>A. \<forall>y\<in>A. x \<sqsubseteq> y \<longrightarrow> x = y\<close>
   obtain x where x: "x \<in> A"
            and x_eq: "\<And>y. \<lbrakk>y \<in> A; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x = y" by fast
   show ?case
@@ -408,7 +408,7 @@
  apply (simp add: choose_pos.simps)
 done
 
-subsubsection {* Compact basis take function *}
+subsubsection \<open>Compact basis take function\<close>
 
 primrec
   cb_take :: "nat \<Rightarrow> 'a compact_basis \<Rightarrow> 'a compact_basis" where
@@ -462,7 +462,7 @@
 apply (rule inj_onI, simp add: Rep_compact_basis_inject)
 done
 
-subsubsection {* Rank of basis elements *}
+subsubsection \<open>Rank of basis elements\<close>
 
 definition
   rank :: "'a compact_basis \<Rightarrow> nat"
@@ -541,7 +541,7 @@
 lemma rank_lt_Un_rank_eq: "rank_lt x \<union> rank_eq x = rank_le x"
 unfolding rank_lt_def rank_eq_def rank_le_def by auto
 
-subsubsection {* Sequencing basis elements *}
+subsubsection \<open>Sequencing basis elements\<close>
 
 definition
   place :: "'a compact_basis \<Rightarrow> nat"
@@ -590,7 +590,7 @@
 lemma inj_place: "inj place"
 by (rule inj_onI, erule place_eqD)
 
-subsubsection {* Embedding and projection on basis elements *}
+subsubsection \<open>Embedding and projection on basis elements\<close>
 
 definition
   sub :: "'a compact_basis \<Rightarrow> 'a compact_basis"
@@ -672,15 +672,15 @@
   show ?case proof (rule linorder_cases)
     assume "place x < place y"
     then have "rank x < rank y"
-      using `x \<sqsubseteq> y` by (rule rank_place_mono)
-    with `place x < place y` show ?case
+      using \<open>x \<sqsubseteq> y\<close> by (rule rank_place_mono)
+    with \<open>place x < place y\<close> show ?case
       apply (case_tac "y = compact_bot", simp)
       apply (simp add: basis_emb.simps [of y])
       apply (rule ubasis_le_trans [OF _ ubasis_le_lower [OF fin2]])
       apply (rule less)
        apply (simp add: less_max_iff_disj)
        apply (erule place_sub_less)
-      apply (erule rank_less_imp_below_sub [OF `x \<sqsubseteq> y`])
+      apply (erule rank_less_imp_below_sub [OF \<open>x \<sqsubseteq> y\<close>])
       done
   next
     assume "place x = place y"
@@ -688,7 +688,7 @@
     thus ?case by (simp add: ubasis_le_refl)
   next
     assume "place x > place y"
-    with `x \<sqsubseteq> y` show ?case
+    with \<open>x \<sqsubseteq> y\<close> show ?case
       apply (case_tac "x = compact_bot", simp add: ubasis_le_minimal)
       apply (simp add: basis_emb.simps [of x])
       apply (rule ubasis_le_upper [OF fin2], simp)
@@ -848,7 +848,7 @@
     by (rule bifinite_approx_chain.ideal_completion)
 qed
 
-subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
+subsubsection \<open>EP-pair from any bifinite domain into \emph{udom}\<close>
 
 context bifinite_approx_chain begin
 
@@ -896,7 +896,7 @@
 lemmas ep_pair_udom =
   bifinite_approx_chain.ep_pair_udom [unfolded bifinite_approx_chain_def]
 
-subsection {* Chain of approx functions for type \emph{udom} *}
+subsection \<open>Chain of approx functions for type \emph{udom}\<close>
 
 definition
   udom_approx :: "nat \<Rightarrow> udom \<rightarrow> udom"
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)
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
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Concurrency_Monad.thy
--- a/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -6,10 +6,10 @@
 imports HOLCF
 begin
 
-text {* This file contains the concurrency monad example from
-  Chapter 7 of the author's PhD thesis. *}
+text \<open>This file contains the concurrency monad example from
+  Chapter 7 of the author's PhD thesis.\<close>
 
-subsection {* State/nondeterminism monad, as a type synonym *}
+subsection \<open>State/nondeterminism monad, as a type synonym\<close>
 
 type_synonym ('s, 'a) N = "'s \<rightarrow> ('a u \<otimes> 's u)\<natural>"
 
@@ -90,7 +90,7 @@
 unfolding plusN_def by (simp add: eta_cfun)
 
 
-subsection {* Resumption-state-nondeterminism monad *}
+subsection \<open>Resumption-state-nondeterminism monad\<close>
 
 domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")
 
@@ -129,7 +129,7 @@
 by (simp add: mapN_def R.take_rews(2))
 
 
-subsection {* Map function *}
+subsection \<open>Map function\<close>
 
 fixrec mapR :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R"
   where "mapR\<cdot>f\<cdot>(Done\<cdot>a) = Done\<cdot>(f\<cdot>a)"
@@ -155,7 +155,7 @@
 done
 
 
-subsection {* Monadic bind function *}
+subsection \<open>Monadic bind function\<close>
 
 fixrec bindR :: "('s, 'a) R \<rightarrow> ('a \<rightarrow> ('s, 'b) R) \<rightarrow> ('s, 'b) R"
   where "bindR\<cdot>(Done\<cdot>x)\<cdot>k = k\<cdot>x"
@@ -178,7 +178,7 @@
 apply (simp_all add: mapN_mapN)
 done
 
-subsection {* Zip function *}
+subsection \<open>Zip function\<close>
 
 fixrec zipR :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R \<rightarrow> ('s, 'c) R"
   where zipR_Done_Done:
@@ -203,7 +203,7 @@
 abbreviation apR (infixl "\<diamondop>" 70)
   where "a \<diamondop> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
 
-text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
+text \<open>Proofs that \<open>zipR\<close> satisfies the applicative functor laws:\<close>
 
 lemma R_homomorphism: "Done\<cdot>f \<diamondop> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
   by simp
@@ -214,7 +214,7 @@
 lemma R_interchange: "r \<diamondop> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamondop> r"
   by (induct r, simp_all add: mapN_mapN)
 
-text {* The associativity rule is the hard one! *}
+text \<open>The associativity rule is the hard one!\<close>
 
 lemma R_associativity: "Done\<cdot>cfcomp \<diamondop> r1 \<diamondop> r2 \<diamondop> r3 = r1 \<diamondop> (r2 \<diamondop> r3)"
 proof (induct r1 arbitrary: r2 r3)
@@ -258,7 +258,7 @@
   qed simp_all
 qed simp_all
 
-text {* Other miscellaneous properties about @{text zipR}: *}
+text \<open>Other miscellaneous properties about \<open>zipR\<close>:\<close>
 
 lemma zipR_Done_left:
   shows "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r = mapR\<cdot>(f\<cdot>x)\<cdot>r"
@@ -358,7 +358,7 @@
  apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
 done
 
-text {* Alternative proof using take lemma. *}
+text \<open>Alternative proof using take lemma.\<close>
 
 lemma
   fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
@@ -398,7 +398,7 @@
             by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
         next
           case (More nC)
-          note H = `a = More\<cdot>nA` `b = More\<cdot>nB` `c = More\<cdot>nC`
+          note H = \<open>a = More\<cdot>nA\<close> \<open>b = More\<cdot>nB\<close> \<open>c = More\<cdot>nC\<close>
           show ?P
             apply (simp only: H zipR_More_More)
             apply (simplesubst zipR_More_More [of f, symmetric])
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Dnat.thy
--- a/src/HOL/HOLCF/ex/Dnat.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Dnat.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -16,9 +16,9 @@
     case n of dzero => x
       | dsucc $ m => f $ (h $ m $ f $ x))"
 
-text {*
+text \<open>
   \medskip Expand fixed point properties.
-*}
+\<close>
 
 lemma iterator_def2:
   "iterator = (LAM n f x. case n of dzero => x | dsucc$m => f$(iterator$m$f$x))"
@@ -29,7 +29,7 @@
   apply simp
   done
 
-text {* \medskip Recursive properties. *}
+text \<open>\medskip Recursive properties.\<close>
 
 lemma iterator1: "iterator $ UU $ f $ x = UU"
   apply (subst iterator_def2)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Internal domain package proofs done manually *}
+section \<open>Internal domain package proofs done manually\<close>
 
 theory Domain_Proofs
 imports HOLCF
@@ -21,9 +21,9 @@
 
 (********************************************************************)
 
-subsection {* Step 1: Define the new type combinators *}
+subsection \<open>Step 1: Define the new type combinators\<close>
 
-text {* Start with the one-step non-recursive version *}
+text \<open>Start with the one-step non-recursive version\<close>
 
 definition
   foo_bar_baz_deflF ::
@@ -42,7 +42,7 @@
 unfolding foo_bar_baz_deflF_def
 by (simp add: split_def)
 
-text {* Individual type combinators are projected from the fixed point. *}
+text \<open>Individual type combinators are projected from the fixed point.\<close>
 
 definition foo_defl :: "udom defl \<rightarrow> udom defl"
 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
@@ -59,7 +59,7 @@
   "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
 
-text {* Unfold rules for each combinator. *}
+text \<open>Unfold rules for each combinator.\<close>
 
 lemma foo_defl_unfold:
   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
@@ -76,9 +76,9 @@
 
 (********************************************************************)
 
-subsection {* Step 2: Define types, prove class instances *}
+subsection \<open>Step 2: Define types, prove class instances\<close>
 
-text {* Use @{text pcpodef} with the appropriate type combinator. *}
+text \<open>Use \<open>pcpodef\<close> with the appropriate type combinator.\<close>
 
 pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
@@ -89,7 +89,7 @@
 pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
-text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
+text \<open>Prove rep instance using lemma \<open>typedef_rep_class\<close>.\<close>
 
 instantiation foo :: ("domain") "domain"
 begin
@@ -196,7 +196,7 @@
 
 end
 
-text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
+text \<open>Prove DEFL rules using lemma \<open>typedef_DEFL\<close>.\<close>
 
 lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"
 apply (rule typedef_DEFL)
@@ -213,7 +213,7 @@
 apply (rule defl_baz_def)
 done
 
-text {* Prove DEFL equations using type combinator unfold lemmas. *}
+text \<open>Prove DEFL equations using type combinator unfold lemmas.\<close>
 
 lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
@@ -229,9 +229,9 @@
 
 (********************************************************************)
 
-subsection {* Step 3: Define rep and abs functions *}
+subsection \<open>Step 3: Define rep and abs functions\<close>
 
-text {* Define them all using @{text prj} and @{text emb}! *}
+text \<open>Define them all using \<open>prj\<close> and \<open>emb\<close>!\<close>
 
 definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
 where "foo_rep \<equiv> prj oo emb"
@@ -251,7 +251,7 @@
 definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
 where "baz_abs \<equiv> prj oo emb"
 
-text {* Prove isomorphism rules. *}
+text \<open>Prove isomorphism rules.\<close>
 
 lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
 by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
@@ -271,7 +271,7 @@
 lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
 by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
 
-text {* Prove isodefl rules using @{text isodefl_coerce}. *}
+text \<open>Prove isodefl rules using \<open>isodefl_coerce\<close>.\<close>
 
 lemma isodefl_foo_abs:
   "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
@@ -287,12 +287,12 @@
 
 (********************************************************************)
 
-subsection {* Step 4: Define map functions, prove isodefl property *}
+subsection \<open>Step 4: Define map functions, prove isodefl property\<close>
 
-text {* Start with the one-step non-recursive version. *}
+text \<open>Start with the one-step non-recursive version.\<close>
 
-text {* Note that the type of the map function depends on which
-variables are used in positive and negative positions. *}
+text \<open>Note that the type of the map function depends on which
+variables are used in positive and negative positions.\<close>
 
 definition
   foo_bar_baz_mapF ::
@@ -325,7 +325,7 @@
 unfolding foo_bar_baz_mapF_def
 by (simp add: split_def)
 
-text {* Individual map functions are projected from the fixed point. *}
+text \<open>Individual map functions are projected from the fixed point.\<close>
 
 definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
 where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
@@ -342,7 +342,7 @@
   "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
 unfolding foo_map_def bar_map_def baz_map_def by simp_all
 
-text {* Prove isodefl rules for all map functions simultaneously. *}
+text \<open>Prove isodefl rules for all map functions simultaneously.\<close>
 
 lemma isodefl_foo_bar_baz:
   assumes isodefl_d: "isodefl d t"
@@ -374,7 +374,7 @@
 lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
 lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
 
-text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
+text \<open>Prove map ID lemmas, using isodefl_DEFL_imp_ID\<close>
 
 lemma foo_map_ID: "foo_map\<cdot>ID = ID"
 apply (rule isodefl_DEFL_imp_ID)
@@ -399,7 +399,7 @@
 
 (********************************************************************)
 
-subsection {* Step 5: Define take functions, prove lub-take lemmas *}
+subsection \<open>Step 5: Define take functions, prove lub-take lemmas\<close>
 
 definition
   foo_bar_baz_takeF ::
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Focus_ex.thy
--- a/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -181,8 +181,8 @@
 done
 
 lemma lemma3: "def_g(g) --> is_g(g)"
-apply (tactic {* simp_tac (put_simpset HOL_ss @{context}
-  addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
+apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
+  addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1\<close>)
 apply (rule impI)
 apply (erule exE)
 apply (rule_tac x = "f" in exI)
@@ -206,9 +206,9 @@
 done
 
 lemma lemma4: "is_g(g) --> def_g(g)"
-apply (tactic {* simp_tac (put_simpset HOL_ss @{context}
+apply (tactic \<open>simp_tac (put_simpset HOL_ss @{context}
   delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
-  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
+  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1\<close>)
 apply (rule impI)
 apply (erule exE)
 apply (rule_tac x = "f" in exI)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* Recursive let bindings *}
+section \<open>Recursive let bindings\<close>
 
 theory Letrec
 imports HOLCF
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Loop.thy
--- a/src/HOL/HOLCF/ex/Loop.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Loop.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-section {* Theory for a loop primitive like while *}
+section \<open>Theory for a loop primitive like while\<close>
 
 theory Loop
 imports HOLCF
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-section {* An experimental pattern-matching notation *}
+section \<open>An experimental pattern-matching notation\<close>
 
 theory Pattern_Match
 imports HOLCF
@@ -10,7 +10,7 @@
 
 default_sort pcpo
 
-text {* FIXME: Find a proper way to un-hide constants. *}
+text \<open>FIXME: Find a proper way to un-hide constants.\<close>
 
 abbreviation fail :: "'a match"
 where "fail \<equiv> Fixrec.fail"
@@ -21,7 +21,7 @@
 abbreviation run :: "'a match \<rightarrow> 'a"
 where "run \<equiv> Fixrec.run"
 
-subsection {* Fatbar combinator *}
+subsection \<open>Fatbar combinator\<close>
 
 definition
   fatbar :: "('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> ('a \<rightarrow> 'b match)" where
@@ -53,7 +53,7 @@
 
 lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
 
-subsection {* Bind operator for match monad *}
+subsection \<open>Bind operator for match monad\<close>
 
 definition match_bind :: "'a match \<rightarrow> ('a \<rightarrow> 'b match) \<rightarrow> 'b match" where
   "match_bind = (\<Lambda> m k. sscase\<cdot>(\<Lambda> _. fail)\<cdot>(fup\<cdot>k)\<cdot>(Rep_match m))"
@@ -66,7 +66,7 @@
 by (simp_all add: cont_Rep_match cont_Abs_match
   Rep_match_strict Abs_match_inverse)
 
-subsection {* Case branch combinator *}
+subsection \<open>Case branch combinator\<close>
 
 definition
   branch :: "('a \<rightarrow> 'b match) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c match)" where
@@ -81,13 +81,13 @@
 lemma branch_succeed [simp]: "branch succeed\<cdot>r\<cdot>x = succeed\<cdot>(r\<cdot>x)"
 by (simp add: branch_def)
 
-subsection {* Cases operator *}
+subsection \<open>Cases operator\<close>
 
 definition
   cases :: "'a match \<rightarrow> 'a::pcpo" where
   "cases = Fixrec.run"
 
-text {* rewrite rules for cases *}
+text \<open>rewrite rules for cases\<close>
 
 lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
 by (simp add: cases_def)
@@ -98,7 +98,7 @@
 lemma cases_succeed [simp]: "cases\<cdot>(succeed\<cdot>x) = x"
 by (simp add: cases_def)
 
-subsection {* Case syntax *}
+subsection \<open>Case syntax\<close>
 
 nonterminal Case_pat and Case_syn and Cases_syn
 
@@ -116,7 +116,7 @@
   "_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
   "_Case2 m ms" == "m \<parallel> ms"
 
-text {* Parsing Case expressions *}
+text \<open>Parsing Case expressions\<close>
 
 syntax
   "_pat" :: "'a"
@@ -128,19 +128,19 @@
   "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
   "_variable _noargs r" => "CONST unit_when\<cdot>r"
 
-parse_translation {*
+parse_translation \<open>
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
   Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
-*}
+\<close>
 
-text {* Printing Case expressions *}
+text \<open>Printing Case expressions\<close>
 
 syntax
   "_match" :: "'a"
 
-print_translation {*
+print_translation \<open>
   let
     fun dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax unit_when},_) $ t) =
           (Syntax.const @{syntax_const "_noargs"}, t)
@@ -165,13 +165,13 @@
           end;
 
   in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
-*}
+\<close>
 
 translations
   "x" <= "_match (CONST succeed) (_variable x)"
 
 
-subsection {* Pattern combinators for data constructors *}
+subsection \<open>Pattern combinators for data constructors\<close>
 
 type_synonym ('a, 'b) pat = "'a \<rightarrow> 'b match"
 
@@ -209,7 +209,7 @@
   ONE_pat :: "(one, unit) pat" where
   "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())"
 
-text {* Parse translations (patterns) *}
+text \<open>Parse translations (patterns)\<close>
 translations
   "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
@@ -220,12 +220,12 @@
   "_pat (XCONST FF)" => "CONST FF_pat"
   "_pat (XCONST ONE)" => "CONST ONE_pat"
 
-text {* CONST version is also needed for constructors with special syntax *}
+text \<open>CONST version is also needed for constructors with special syntax\<close>
 translations
   "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)"
   "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
 
-text {* Parse translations (variables) *}
+text \<open>Parse translations (variables)\<close>
 translations
   "_variable (XCONST Pair x y) r" => "_variable (_args x y) r"
   "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
@@ -240,7 +240,7 @@
   "_variable (CONST Pair x y) r" => "_variable (_args x y) r"
   "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
 
-text {* Print translations *}
+text \<open>Print translations\<close>
 translations
   "CONST Pair (_match p1 v1) (_match p2 v2)"
       <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)"
@@ -318,7 +318,7 @@
 by (simp_all add: branch_def ONE_pat_def)
 
 
-subsection {* Wildcards, as-patterns, and lazy patterns *}
+subsection \<open>Wildcards, as-patterns, and lazy patterns\<close>
 
 definition
   wild_pat :: "'a \<rightarrow> unit match" where
@@ -332,15 +332,15 @@
   lazy_pat :: "('a \<rightarrow> 'b::pcpo match) \<Rightarrow> ('a \<rightarrow> 'b match)" where
   "lazy_pat p = (\<Lambda> x. succeed\<cdot>(cases\<cdot>(p\<cdot>x)))"
 
-text {* Parse translations (patterns) *}
+text \<open>Parse translations (patterns)\<close>
 translations
   "_pat _" => "CONST wild_pat"
 
-text {* Parse translations (variables) *}
+text \<open>Parse translations (variables)\<close>
 translations
   "_variable _ r" => "_variable _noargs r"
 
-text {* Print translations *}
+text \<open>Print translations\<close>
 translations
   "_" <= "_match (CONST wild_pat) _noargs"
 
@@ -361,7 +361,7 @@
 apply (cases "p\<cdot>x", simp_all)+
 done
 
-subsection {* Examples *}
+subsection \<open>Examples\<close>
 
 term "Case t of (:up\<cdot>(sinl\<cdot>x), sinr\<cdot>y:) \<Rightarrow> (x, y)"
 
@@ -369,9 +369,9 @@
 
 term "\<Lambda> t. Case t of (:up\<cdot>(sinl\<cdot>_), sinr\<cdot>x:) \<Rightarrow> x"
 
-subsection {* ML code for generating definitions *}
+subsection \<open>ML code for generating definitions\<close>
 
-ML {*
+ML \<open>
 local open HOLCF_Library in
 
 infixr 6 ->>;
@@ -586,7 +586,7 @@
   end
 
 end
-*}
+\<close>
 
 (*
 Cut from HOLCF/Tools/domain_constructors.ML
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,13 +2,13 @@
     Author:     Brian Huffman
 *)
 
-section {* Powerdomain examples *}
+section \<open>Powerdomain examples\<close>
 
 theory Powerdomain_ex
 imports HOLCF
 begin
 
-subsection {* Monadic sorting example *}
+subsection \<open>Monadic sorting example\<close>
 
 domain ordering = LT | EQ | GT
 
@@ -43,7 +43,7 @@
 done
 
 
-subsection {* Picking a leaf from a tree *}
+subsection \<open>Picking a leaf from a tree\<close>
 
 domain 'a tree =
   Node (lazy "'a tree") (lazy "'a tree") |
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -183,7 +183,7 @@
   {
     fix b
     assume "b \<in> as"
-    hence id2: "insert a as - {b} = insert a (as - {b})" using `a \<notin> as` by auto
+    hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto
     have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
       unfolding id2
       by (subst setprod.insert, insert insert, auto)
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/List.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -5399,7 +5399,7 @@
 apply (case_tac xys, simp_all, blast)
 done
 
-text{* By Mathias Fleury: *}
+text\<open>By Mathias Fleury:\<close>
 lemma lexn_transI:
   assumes "trans r" shows "trans (lexn r n)"
 unfolding trans_def
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -6056,7 +6056,7 @@
      apply (clarsimp simp del: divide_const_simps)
      apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
      done
-  --\<open>Replacing @{term r} and the original (weak) premises\<close>
+  \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close>
   obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
     apply (rule that [of "(r + dist w z) / 2"])
       apply (simp_all add: fh')
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -272,7 +272,7 @@
   qed
 qed
 
-text{*Alternative version, formulated as in HOL Light*}
+text\<open>Alternative version, formulated as in HOL Light\<close>
 corollary series_comparison_uniform:
   fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
   assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Multivariate_Analysis/ex/Approximations.thy
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -530,13 +530,13 @@
   shows   "\<bar>pi - pi_approx n\<bar> \<le> inverse (2^(13*n - 2))"
 proof -
   from n have n': "even (3*n)" by simp
-  -- \<open>We apply the Machin formula\<close>
+  \<comment> \<open>We apply the Machin formula\<close>
   from machin have "pi = 16 * arctan (1/5) - 4 * arctan (1/239::real)" by simp
-  -- \<open>Taylor series expansion of the arctangent\<close>
+  \<comment> \<open>Taylor series expansion of the arctangent\<close>
   also from arctan_approx[OF _ _ n', of "1/5"] arctan_approx[OF _ _ n, of "1/239"]
     have "\<dots> - pi_approx n \<in> {-4*((1/239)^(2*n+1) / (1-(1/239)^4))..16*(1/5)^(6*n+1) / (1-(1/5)^4)}"
     by (simp add: pi_approx_def)
-  -- \<open>Coarsening the bounds to make them a bit nicer\<close>
+  \<comment> \<open>Coarsening the bounds to make them a bit nicer\<close>
   also have "-4*((1/239::real)^(2*n+1) / (1-(1/239)^4)) = -((13651919 / 815702160) / 57121^n)"
     by (simp add: power_mult power2_eq_square) (simp add: field_simps)
   also have "16*(1/5)^(6*n+1) / (1-(1/5::real)^4) = (125/39) / 15625^n"
@@ -561,11 +561,11 @@
 proof -
   def a \<equiv> "8295936325956147794769600190539918304 / 2626685325478320010006427764892578125 :: real"
   def b \<equiv> "8428294561696506782041394632 / 503593538783547230635598424135 :: real"
-  -- \<open>The introduction of this constant prevents the simplifier from applying solvers that
+  \<comment> \<open>The introduction of this constant prevents the simplifier from applying solvers that
       we don't want. We want it to simply evaluate the terms to rational constants.}\<close>
   def eq \<equiv> "op = :: real \<Rightarrow> real \<Rightarrow> bool"
 
-  -- \<open>Splitting the computation into several steps has the advantage that simplification can
+  \<comment> \<open>Splitting the computation into several steps has the advantage that simplification can
       be done in parallel\<close>
   have "abs (pi - pi_approx 6) \<le> inverse (2^76)" by (rule pi_approx') simp_all
   also have "pi_approx 6 = 16 * arctan_approx (3 * 6) (1 / 5) - 4 * arctan_approx 6 (1 / 239)"
@@ -694,7 +694,7 @@
     by (unfold a_def b_def c_def, simp, unfold eq_def, rule refl)
   also have [unfolded eq_def]: "eq (\<dots> - c) ?pi''"
     by (unfold a_def b_def c_def, simp, unfold eq_def, rule refl)
-  -- \<open>This is incredibly slow because the numerators and denominators are huge.\<close>
+  \<comment> \<open>This is incredibly slow because the numerators and denominators are huge.\<close>
   finally show ?thesis by (rule approx_coarsen) simp
 qed
 
diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2506,7 +2506,7 @@
   fix E assume "eventually E uniformity"
   with M obtain X where "\<forall>S\<in>M. finite (X S) \<and> (\<forall>s\<in>S. \<exists>x\<in>X S. E (x, s))"
     by (metis totally_bounded_def)
-  with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
+  with \<open>finite M\<close> show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
     by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
 qed