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 ::
```