src/HOL/HOLCF/Powerdomains.thy
 changeset 62175 8ffc4d0e652d parent 58880 0baae4311a9f child 69597 ff784d5a5bfb
```     1.1 --- a/src/HOL/HOLCF/Powerdomains.thy	Wed Jan 13 23:02:28 2016 +0100
1.2 +++ b/src/HOL/HOLCF/Powerdomains.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 {* Powerdomains *}
1.8 +section \<open>Powerdomains\<close>
1.9
1.10  theory Powerdomains
1.11  imports ConvexPD Domain
1.12  begin
1.13
1.14 -subsection {* Universal domain embeddings *}
1.15 +subsection \<open>Universal domain embeddings\<close>
1.16
1.17  definition "upper_emb = udom_emb (\<lambda>i. upper_map\<cdot>(udom_approx i))"
1.18  definition "upper_prj = udom_prj (\<lambda>i. upper_map\<cdot>(udom_approx i))"
1.19 @@ -31,7 +31,7 @@
1.20    unfolding convex_emb_def convex_prj_def
1.21    by (simp add: ep_pair_udom approx_chain_convex_map)
1.22
1.23 -subsection {* Deflation combinators *}
1.24 +subsection \<open>Deflation combinators\<close>
1.25
1.26  definition upper_defl :: "udom defl \<rightarrow> udom defl"
1.27    where "upper_defl = defl_fun1 upper_emb upper_prj upper_map"
1.28 @@ -57,7 +57,7 @@
1.29  using ep_pair_convex finite_deflation_convex_map
1.30  unfolding convex_defl_def by (rule cast_defl_fun1)
1.31
1.32 -subsection {* Domain class instances *}
1.33 +subsection \<open>Domain class instances\<close>
1.34
1.35  instantiation upper_pd :: ("domain") "domain"
1.36  begin
1.37 @@ -167,7 +167,7 @@
1.38  lemma DEFL_convex: "DEFL('a::domain convex_pd) = convex_defl\<cdot>DEFL('a)"
1.39  by (rule defl_convex_pd_def)
1.40
1.41 -subsection {* Isomorphic deflations *}
1.42 +subsection \<open>Isomorphic deflations\<close>
1.43
1.44  lemma isodefl_upper:
1.45    "isodefl d t \<Longrightarrow> isodefl (upper_map\<cdot>d) (upper_defl\<cdot>t)"
1.46 @@ -193,7 +193,7 @@
1.48  done
1.49
1.50 -subsection {* Domain package setup for powerdomains *}
1.51 +subsection \<open>Domain package setup for powerdomains\<close>
1.52
1.53  lemmas [domain_defl_simps] = DEFL_upper DEFL_lower DEFL_convex
1.54  lemmas [domain_map_ID] = upper_map_ID lower_map_ID convex_map_ID
1.55 @@ -202,11 +202,11 @@
1.56  lemmas [domain_deflation] =
1.57    deflation_upper_map deflation_lower_map deflation_convex_map
1.58
1.59 -setup {*
1.60 +setup \<open>