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.47  apply (simp add: convex_map_map)
    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>
    1.61    fold Domain_Take_Proofs.add_rec_type
    1.62      [(@{type_name "upper_pd"}, [true]),
    1.63       (@{type_name "lower_pd"}, [true]),
    1.64       (@{type_name "convex_pd"}, [true])]
    1.65 -*}
    1.66 +\<close>
    1.67  
    1.68  end