src/HOL/HOLCF/Algebraic.thy
changeset 62175 8ffc4d0e652d
parent 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Algebraic.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Algebraic.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Algebraic deflations *}
     1.8 +section \<open>Algebraic deflations\<close>
     1.9  
    1.10  theory Algebraic
    1.11  imports Universal Map_Functions
    1.12 @@ -10,7 +10,7 @@
    1.13  
    1.14  default_sort bifinite
    1.15  
    1.16 -subsection {* Type constructor for finite deflations *}
    1.17 +subsection \<open>Type constructor for finite deflations\<close>
    1.18  
    1.19  typedef 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
    1.20  by (fast intro: finite_deflation_bottom)
    1.21 @@ -72,7 +72,7 @@
    1.22  using finite_deflation_Rep_fin_defl
    1.23  by (rule finite_deflation_imp_compact)
    1.24  
    1.25 -subsection {* Defining algebraic deflations by ideal completion *}
    1.26 +subsection \<open>Defining algebraic deflations by ideal completion\<close>
    1.27  
    1.28  typedef 'a defl = "{S::'a fin_defl set. below.ideal S}"
    1.29  by (rule below.ex_ideal)
    1.30 @@ -132,7 +132,7 @@
    1.31  using defl_principal_def fin_defl_countable
    1.32  by (rule below.typedef_ideal_completion)
    1.33  
    1.34 -text {* Algebraic deflations are pointed *}
    1.35 +text \<open>Algebraic deflations are pointed\<close>
    1.36  
    1.37  lemma defl_minimal: "defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
    1.38  apply (induct x rule: defl.principal_induct, simp)
    1.39 @@ -147,7 +147,7 @@
    1.40  lemma inst_defl_pcpo: "\<bottom> = defl_principal (Abs_fin_defl \<bottom>)"
    1.41  by (rule defl_minimal [THEN bottomI, symmetric])
    1.42  
    1.43 -subsection {* Applying algebraic deflations *}
    1.44 +subsection \<open>Applying algebraic deflations\<close>
    1.45  
    1.46  definition
    1.47    cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
    1.48 @@ -215,7 +215,7 @@
    1.49  lemma cast_strict2 [simp]: "cast\<cdot>A\<cdot>\<bottom> = \<bottom>"
    1.50  by (rule cast.below [THEN bottomI])
    1.51  
    1.52 -subsection {* Deflation combinators *}
    1.53 +subsection \<open>Deflation combinators\<close>
    1.54  
    1.55  definition
    1.56    "defl_fun1 e p f =