src/HOL/HOLCF/Map_Functions.thy
changeset 62175 8ffc4d0e652d
parent 61169 4de9ff3ea29a
child 65380 ae93953746fc
     1.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Brian Huffman
     1.5  *)
     1.6  
     1.7 -section {* Map functions for various types *}
     1.8 +section \<open>Map functions for various types\<close>
     1.9  
    1.10  theory Map_Functions
    1.11  imports Deflation
    1.12  begin
    1.13  
    1.14 -subsection {* Map operator for continuous function space *}
    1.15 +subsection \<open>Map operator for continuous function space\<close>
    1.16  
    1.17  default_sort cpo
    1.18  
    1.19 @@ -105,7 +105,7 @@
    1.20      by (rule finite_range_imp_finite_fixes)
    1.21  qed
    1.22  
    1.23 -text {* Finite deflations are compact elements of the function space *}
    1.24 +text \<open>Finite deflations are compact elements of the function space\<close>
    1.25  
    1.26  lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d"
    1.27  apply (frule finite_deflation_imp_deflation)
    1.28 @@ -115,7 +115,7 @@
    1.29  apply (simp only: finite_deflation_cfun_map)
    1.30  done
    1.31  
    1.32 -subsection {* Map operator for product type *}
    1.33 +subsection \<open>Map operator for product type\<close>
    1.34  
    1.35  definition
    1.36    prod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    1.37 @@ -172,7 +172,7 @@
    1.38      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.39  qed
    1.40  
    1.41 -subsection {* Map function for lifted cpo *}
    1.42 +subsection \<open>Map function for lifted cpo\<close>
    1.43  
    1.44  definition
    1.45    u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u"
    1.46 @@ -218,7 +218,7 @@
    1.47      by (rule finite_subset, simp add: d.finite_fixes)
    1.48  qed
    1.49  
    1.50 -subsection {* Map function for strict products *}
    1.51 +subsection \<open>Map function for strict products\<close>
    1.52  
    1.53  default_sort pcpo
    1.54  
    1.55 @@ -299,7 +299,7 @@
    1.56      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.57  qed
    1.58  
    1.59 -subsection {* Map function for strict sums *}
    1.60 +subsection \<open>Map function for strict sums\<close>
    1.61  
    1.62  definition
    1.63    ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd"
    1.64 @@ -383,7 +383,7 @@
    1.65      by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    1.66  qed
    1.67  
    1.68 -subsection {* Map operator for strict function space *}
    1.69 +subsection \<open>Map operator for strict function space\<close>
    1.70  
    1.71  definition
    1.72    sfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow>! 'c) \<rightarrow> ('b \<rightarrow>! 'd)"
    1.73 @@ -461,7 +461,7 @@
    1.74    then show "finite {f. sfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}"
    1.75      unfolding sfun_map_def sfun_eq_iff
    1.76      by (simp add: strictify_cancel
    1.77 -         deflation_strict `deflation d1` `deflation d2`)
    1.78 +         deflation_strict \<open>deflation d1\<close> \<open>deflation d2\<close>)
    1.79  qed
    1.80  
    1.81  end