--- 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 =