src/HOL/HOLCF/Compact_Basis.thy
changeset 62175 8ffc4d0e652d
parent 59797 f313ca9fbba0
     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Compact_Basis.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 {* A compact basis for powerdomains *}
     1.8 +section \<open>A compact basis for powerdomains\<close>
     1.9  
    1.10  theory Compact_Basis
    1.11  imports Universal
    1.12 @@ -10,7 +10,7 @@
    1.13  
    1.14  default_sort bifinite
    1.15  
    1.16 -subsection {* A compact basis for powerdomains *}
    1.17 +subsection \<open>A compact basis for powerdomains\<close>
    1.18  
    1.19  definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
    1.20  
    1.21 @@ -26,7 +26,7 @@
    1.22  lemma Rep_pd_basis_nonempty [simp]: "Rep_pd_basis u \<noteq> {}"
    1.23  by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
    1.24  
    1.25 -text {* The powerdomain basis type is countable. *}
    1.26 +text \<open>The powerdomain basis type is countable.\<close>
    1.27  
    1.28  lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
    1.29  proof -
    1.30 @@ -40,7 +40,7 @@
    1.31    (* FIXME: why doesn't ".." or "by (rule exI)" work? *)
    1.32  qed
    1.33  
    1.34 -subsection {* Unit and plus constructors *}
    1.35 +subsection \<open>Unit and plus constructors\<close>
    1.36  
    1.37  definition
    1.38    PDUnit :: "'a compact_basis \<Rightarrow> 'a pd_basis" where
    1.39 @@ -91,7 +91,7 @@
    1.40  apply (rule PDUnit, erule PDPlus [OF PDUnit])
    1.41  done
    1.42  
    1.43 -subsection {* Fold operator *}
    1.44 +subsection \<open>Fold operator\<close>
    1.45  
    1.46  definition
    1.47    fold_pd ::