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