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"