--- a/src/HOLCF/Bifinite.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Bifinite.thy Fri Oct 08 07:39:50 2010 -0700
@@ -8,14 +8,14 @@
imports Algebraic
begin
-subsection {* Class of SFP domains *}
+subsection {* Class of bifinite domains *}
text {*
- We define a SFP domain as a pcpo that is isomorphic to some
+ We define a bifinite domain as a pcpo that is isomorphic to some
algebraic deflation over the universal domain.
*}
-class sfp = pcpo +
+class bifinite = pcpo +
fixes emb :: "'a::pcpo \<rightarrow> udom"
fixes prj :: "udom \<rightarrow> 'a::pcpo"
fixes sfp :: "'a itself \<Rightarrow> sfp"
@@ -25,26 +25,26 @@
syntax "_SFP" :: "type \<Rightarrow> sfp" ("(1SFP/(1'(_')))")
translations "SFP('t)" \<rightleftharpoons> "CONST sfp TYPE('t)"
-interpretation sfp:
- pcpo_ep_pair "emb :: 'a::sfp \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::sfp"
+interpretation bifinite:
+ pcpo_ep_pair "emb :: 'a::bifinite \<rightarrow> udom" "prj :: udom \<rightarrow> 'a::bifinite"
unfolding pcpo_ep_pair_def
by (rule ep_pair_emb_prj)
-lemmas emb_inverse = sfp.e_inverse
-lemmas emb_prj_below = sfp.e_p_below
-lemmas emb_eq_iff = sfp.e_eq_iff
-lemmas emb_strict = sfp.e_strict
-lemmas prj_strict = sfp.p_strict
+lemmas emb_inverse = bifinite.e_inverse
+lemmas emb_prj_below = bifinite.e_p_below
+lemmas emb_eq_iff = bifinite.e_eq_iff
+lemmas emb_strict = bifinite.e_strict
+lemmas prj_strict = bifinite.p_strict
-subsection {* SFP domains have a countable compact basis *}
+subsection {* Bifinite domains have a countable compact basis *}
text {*
Eventually it should be possible to generalize this to an unpointed
- variant of the sfp class.
+ variant of the bifinite class.
*}
interpretation compact_basis:
- ideal_completion below Rep_compact_basis "approximants::'a::sfp \<Rightarrow> _"
+ ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _"
proof -
obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)"
and SFP: "SFP('a) = (\<Squnion>i. sfp_principal (Y i))"
@@ -59,7 +59,7 @@
by (simp add: lub_distribs Y SFP [symmetric] cast_SFP expand_cfun_eq)
show "\<And>i. finite_deflation (approx i)"
unfolding approx_def
- apply (rule sfp.finite_deflation_p_d_e)
+ apply (rule bifinite.finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (rule sfp.compact_principal)
apply (rule below_trans [OF monofun_cfun_fun])
@@ -146,7 +146,7 @@
subsection {* Instance for universal domain type *}
-instantiation udom :: sfp
+instantiation udom :: bifinite
begin
definition [simp]:
@@ -208,7 +208,7 @@
apply (erule (1) finite_deflation_cfun_map)
done
-instantiation cfun :: (sfp, sfp) sfp
+instantiation cfun :: (bifinite, bifinite) bifinite
begin
definition
@@ -233,7 +233,8 @@
end
-lemma SFP_cfun: "SFP('a::sfp \<rightarrow> 'b::sfp) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_cfun:
+ "SFP('a::bifinite \<rightarrow> 'b::bifinite) = cfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_cfun_def)
end
--- a/src/HOLCF/CompactBasis.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
imports Bifinite
begin
-default_sort sfp
+default_sort bifinite
subsection {* A compact basis for powerdomains *}
@@ -24,7 +24,7 @@
text {* The powerdomain basis type is countable. *}
-lemma pd_basis_countable: "\<exists>f::'a::sfp pd_basis \<Rightarrow> nat. inj f"
+lemma pd_basis_countable: "\<exists>f::'a pd_basis \<Rightarrow> nat. inj f"
proof -
obtain g :: "'a compact_basis \<Rightarrow> nat" where "inj g"
using compact_basis.countable ..
--- a/src/HOLCF/ConvexPD.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy Fri Oct 08 07:39:50 2010 -0700
@@ -123,7 +123,7 @@
"{S::'a pd_basis set. convex_le.ideal S}"
by (fast intro: convex_le.ideal_principal)
-instantiation convex_pd :: (sfp) below
+instantiation convex_pd :: (bifinite) below
begin
definition
@@ -132,11 +132,11 @@
instance ..
end
-instance convex_pd :: (sfp) po
+instance convex_pd :: (bifinite) po
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_po)
-instance convex_pd :: (sfp) cpo
+instance convex_pd :: (bifinite) cpo
using type_definition_convex_pd below_convex_pd_def
by (rule convex_le.typedef_ideal_cpo)
@@ -155,7 +155,7 @@
lemma convex_pd_minimal: "convex_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: convex_pd.principal_induct, simp, simp)
-instance convex_pd :: (sfp) pcpo
+instance convex_pd :: (bifinite) pcpo
by intro_classes (fast intro: convex_pd_minimal)
lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
@@ -444,7 +444,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Convex powerdomain is an SFP domain *}
+subsection {* Convex powerdomain is a bifinite domain *}
definition
convex_approx :: "nat \<Rightarrow> udom convex_pd \<rightarrow> udom convex_pd"
@@ -474,7 +474,7 @@
apply (erule finite_deflation_convex_map)
done
-instantiation convex_pd :: (sfp) sfp
+instantiation convex_pd :: (bifinite) bifinite
begin
definition
--- a/src/HOLCF/Cprod.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Cprod.thy Fri Oct 08 07:39:50 2010 -0700
@@ -97,7 +97,7 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Cartesian product is an SFP domain *}
+subsection {* Cartesian product is a bifinite domain *}
definition
prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
@@ -127,7 +127,7 @@
apply (erule (1) finite_deflation_cprod_map)
done
-instantiation prod :: (sfp, sfp) sfp
+instantiation prod :: (bifinite, bifinite) bifinite
begin
definition
@@ -152,7 +152,8 @@
end
-lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_prod:
+ "SFP('a::bifinite \<times> 'b::bifinite) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_prod_def)
end
--- a/src/HOLCF/Library/Strict_Fun.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy Fri Oct 08 07:39:50 2010 -0700
@@ -143,7 +143,7 @@
deflation_strict `deflation d1` `deflation d2`)
qed
-subsection {* Strict function space is an SFP domain *}
+subsection {* Strict function space is a bifinite domain *}
definition
sfun_approx :: "nat \<Rightarrow> (udom \<rightarrow>! udom) \<rightarrow> (udom \<rightarrow>! udom)"
@@ -173,7 +173,7 @@
apply (erule (1) finite_deflation_sfun_map)
done
-instantiation sfun :: (sfp, sfp) sfp
+instantiation sfun :: (bifinite, bifinite) bifinite
begin
definition
@@ -198,9 +198,8 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sfun: "SFP('a::sfp \<rightarrow>! 'b::sfp) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sfun:
+ "SFP('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_sfun_def)
lemma isodefl_sfun:
--- a/src/HOLCF/Lift.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Lift.thy Fri Oct 08 07:39:50 2010 -0700
@@ -171,7 +171,7 @@
by (cases x, simp_all)
-subsection {* Lifted countable types are SFP domains *}
+subsection {* Lifted countable types are bifinite domains *}
definition
lift_approx :: "nat \<Rightarrow> 'a::countable lift \<rightarrow> 'a lift"
@@ -220,7 +220,7 @@
using chain_lift_approx lub_lift_approx finite_deflation_lift_approx
by (rule approx_chain.intro)
-instantiation lift :: (countable) sfp
+instantiation lift :: (countable) bifinite
begin
definition
--- a/src/HOLCF/LowerPD.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/LowerPD.thy Fri Oct 08 07:39:50 2010 -0700
@@ -78,7 +78,7 @@
"{S::'a pd_basis set. lower_le.ideal S}"
by (fast intro: lower_le.ideal_principal)
-instantiation lower_pd :: (sfp) below
+instantiation lower_pd :: (bifinite) below
begin
definition
@@ -87,11 +87,11 @@
instance ..
end
-instance lower_pd :: (sfp) po
+instance lower_pd :: (bifinite) po
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_po)
-instance lower_pd :: (sfp) cpo
+instance lower_pd :: (bifinite) cpo
using type_definition_lower_pd below_lower_pd_def
by (rule lower_le.typedef_ideal_cpo)
@@ -110,7 +110,7 @@
lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: lower_pd.principal_induct, simp, simp)
-instance lower_pd :: (sfp) pcpo
+instance lower_pd :: (bifinite) pcpo
by intro_classes (fast intro: lower_pd_minimal)
lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
@@ -433,7 +433,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Lower powerdomain is an SFP domain *}
+subsection {* Lower powerdomain is a bifinite domain *}
definition
lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd"
@@ -463,7 +463,7 @@
apply (erule finite_deflation_lower_map)
done
-instantiation lower_pd :: (sfp) sfp
+instantiation lower_pd :: (bifinite) bifinite
begin
definition
@@ -488,8 +488,6 @@
end
-text {* SFP of type constructor = type combinator *}
-
lemma SFP_lower: "SFP('a lower_pd) = lower_sfp\<cdot>SFP('a)"
by (rule sfp_lower_pd_def)
--- a/src/HOLCF/Representable.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Representable.thy Fri Oct 08 07:39:50 2010 -0700
@@ -11,23 +11,23 @@
("Tools/Domain/domain_isomorphism.ML")
begin
-default_sort sfp
+default_sort bifinite
subsection {* Representations of types *}
-lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a::sfp) = cast\<cdot>SFP('a)\<cdot>x"
+lemma emb_prj: "emb\<cdot>((prj\<cdot>x)::'a) = cast\<cdot>SFP('a)\<cdot>x"
by (simp add: cast_SFP)
lemma in_SFP_iff:
- "x ::: SFP('a::sfp) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+ "x ::: SFP('a) \<longleftrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
by (simp add: in_sfp_def cast_SFP)
lemma prj_inverse:
- "x ::: SFP('a::sfp) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
+ "x ::: SFP('a) \<Longrightarrow> emb\<cdot>((prj\<cdot>x)::'a) = x"
by (simp only: in_SFP_iff)
lemma emb_in_SFP [simp]:
- "emb\<cdot>(x::'a::sfp) ::: SFP('a)"
+ "emb\<cdot>(x::'a) ::: SFP('a)"
by (simp add: in_SFP_iff)
subsection {* Coerce operator *}
@@ -137,7 +137,7 @@
assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
assumes sfp: "sfp \<equiv> (\<lambda> a::'a itself. t)"
- shows "OFCLASS('a, sfp_class)"
+ shows "OFCLASS('a, bifinite_class)"
proof
have adm: "adm (\<lambda>x. x \<in> {x. x ::: t})"
by (simp add: adm_in_sfp)
@@ -180,13 +180,13 @@
text {* Restore original typing constraints *}
setup {* Sign.add_const_constraint
- (@{const_name sfp}, SOME @{typ "'a::sfp itself \<Rightarrow> sfp"}) *}
+ (@{const_name sfp}, SOME @{typ "'a::bifinite itself \<Rightarrow> sfp"}) *}
setup {* Sign.add_const_constraint
- (@{const_name emb}, SOME @{typ "'a::sfp \<rightarrow> udom"}) *}
+ (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) *}
setup {* Sign.add_const_constraint
- (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::sfp"}) *}
+ (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) *}
lemma adm_mem_Collect_in_sfp: "adm (\<lambda>x. x \<in> {x. x ::: A})"
unfolding mem_Collect_eq by (rule adm_in_sfp)
@@ -196,7 +196,7 @@
subsection {* Isomorphic deflations *}
definition
- isodefl :: "('a::sfp \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
+ isodefl :: "('a \<rightarrow> 'a) \<Rightarrow> sfp \<Rightarrow> bool"
where
"isodefl d t \<longleftrightarrow> cast\<cdot>t = emb oo d oo prj"
@@ -211,7 +211,7 @@
by (drule cfun_fun_cong [where x="\<bottom>"], simp)
lemma isodefl_imp_deflation:
- fixes d :: "'a::sfp \<rightarrow> 'a"
+ fixes d :: "'a \<rightarrow> 'a"
assumes "isodefl d t" shows "deflation d"
proof
note assms [unfolded isodefl_def, simp]
--- a/src/HOLCF/Sprod.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Sprod.thy Fri Oct 08 07:39:50 2010 -0700
@@ -310,7 +310,7 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict product is an SFP domain *}
+subsection {* Strict product is a bifinite domain *}
definition
sprod_approx :: "nat \<Rightarrow> udom \<otimes> udom \<rightarrow> udom \<otimes> udom"
@@ -342,7 +342,7 @@
apply (erule (1) finite_deflation_sprod_map)
done
-instantiation sprod :: (sfp, sfp) sfp
+instantiation sprod :: (bifinite, bifinite) bifinite
begin
definition
@@ -367,9 +367,8 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_sprod: "SFP('a::sfp \<otimes> 'b::sfp) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_sprod:
+ "SFP('a::bifinite \<otimes> 'b::bifinite) = sprod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_sprod_def)
end
--- a/src/HOLCF/Ssum.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Ssum.thy Fri Oct 08 07:39:50 2010 -0700
@@ -295,7 +295,7 @@
by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
qed
-subsection {* Strict sum is an SFP domain *}
+subsection {* Strict sum is a bifinite domain *}
definition
ssum_approx :: "nat \<Rightarrow> udom \<oplus> udom \<rightarrow> udom \<oplus> udom"
@@ -325,7 +325,7 @@
apply (erule (1) finite_deflation_ssum_map)
done
-instantiation ssum :: (sfp, sfp) sfp
+instantiation ssum :: (bifinite, bifinite) bifinite
begin
definition
@@ -350,9 +350,8 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_ssum: "SFP('a::sfp \<oplus> 'b::sfp) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
+lemma SFP_ssum:
+ "SFP('a::bifinite \<oplus> 'b::bifinite) = ssum_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
by (rule sfp_ssum_def)
end
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Oct 08 07:39:50 2010 -0700
@@ -213,7 +213,7 @@
end;
fun pcpo_arg lazy = if lazy then @{sort cpo} else @{sort pcpo};
-fun rep_arg lazy = @{sort sfp};
+fun rep_arg lazy = @{sort bifinite};
val add_domain =
gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms pcpo_arg;
--- a/src/HOLCF/Tools/repdef.ML Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML Fri Oct 08 07:39:50 2010 -0700
@@ -108,7 +108,7 @@
(*instantiate class rep*)
val lthy = thy
- |> Class.instantiation ([full_tname], lhs_tfrees, @{sort sfp});
+ |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
val ((_, (_, emb_ldef)), lthy) =
Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
val ((_, (_, prj_ldef)), lthy) =
--- a/src/HOLCF/Tutorial/New_Domain.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Tutorial/New_Domain.thy Fri Oct 08 07:39:50 2010 -0700
@@ -9,14 +9,14 @@
begin
text {*
- The definitional domain package only works with SFP domains,
- i.e. types in class @{text sfp}.
+ The definitional domain package only works with bifinite domains,
+ i.e. types in class @{text bifinite}.
*}
-default_sort sfp
+default_sort bifinite
text {*
- Provided that @{text sfp} is the default sort, the @{text new_domain}
+ Provided that @{text bifinite} is the default sort, the @{text new_domain}
package should work with any type definition supported by the old
domain package.
*}
--- a/src/HOLCF/Up.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/Up.thy Fri Oct 08 07:39:50 2010 -0700
@@ -332,7 +332,7 @@
by (rule finite_subset, simp add: d.finite_fixes)
qed
-subsection {* Lifted cpo is an SFP domain *}
+subsection {* Lifted cpo is a bifinite domain *}
definition u_approx :: "nat \<Rightarrow> udom\<^sub>\<bottom> \<rightarrow> udom\<^sub>\<bottom>"
where "u_approx = (\<lambda>i. u_map\<cdot>(udom_approx i))"
@@ -360,7 +360,7 @@
apply (erule finite_deflation_u_map)
done
-instantiation u :: (sfp) sfp
+instantiation u :: (bifinite) bifinite
begin
definition
@@ -385,9 +385,7 @@
end
-text {* SFP of type constructor = type combinator *}
-
-lemma SFP_u: "SFP('a::sfp u) = u_sfp\<cdot>SFP('a)"
+lemma SFP_u: "SFP('a::bifinite u) = u_sfp\<cdot>SFP('a)"
by (rule sfp_u_def)
end
--- a/src/HOLCF/UpperPD.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/UpperPD.thy Fri Oct 08 07:39:50 2010 -0700
@@ -76,7 +76,7 @@
"{S::'a pd_basis set. upper_le.ideal S}"
by (fast intro: upper_le.ideal_principal)
-instantiation upper_pd :: (sfp) below
+instantiation upper_pd :: (bifinite) below
begin
definition
@@ -85,11 +85,11 @@
instance ..
end
-instance upper_pd :: (sfp) po
+instance upper_pd :: (bifinite) po
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_po)
-instance upper_pd :: (sfp) cpo
+instance upper_pd :: (bifinite) cpo
using type_definition_upper_pd below_upper_pd_def
by (rule upper_le.typedef_ideal_cpo)
@@ -108,7 +108,7 @@
lemma upper_pd_minimal: "upper_principal (PDUnit compact_bot) \<sqsubseteq> ys"
by (induct ys rule: upper_pd.principal_induct, simp, simp)
-instance upper_pd :: (sfp) pcpo
+instance upper_pd :: (bifinite) pcpo
by intro_classes (fast intro: upper_pd_minimal)
lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
@@ -428,7 +428,7 @@
by (rule finite_range_imp_finite_fixes)
qed
-subsection {* Upper powerdomain is an SFP domain *}
+subsection {* Upper powerdomain is a bifinite domain *}
definition
upper_approx :: "nat \<Rightarrow> udom upper_pd \<rightarrow> udom upper_pd"
@@ -458,7 +458,7 @@
apply (erule finite_deflation_upper_map)
done
-instantiation upper_pd :: (sfp) sfp
+instantiation upper_pd :: (bifinite) bifinite
begin
definition
@@ -483,8 +483,6 @@
end
-text {* SFP of type constructor = type combinator *}
-
lemma SFP_upper: "SFP('a upper_pd) = upper_sfp\<cdot>SFP('a)"
by (rule sfp_upper_pd_def)
--- a/src/HOLCF/ex/Domain_Proofs.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
imports HOLCF
begin
-default_sort sfp
+default_sort bifinite
(*
@@ -93,7 +93,7 @@
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (sfp) sfp
+instantiation foo :: (bifinite) bifinite
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -116,7 +116,7 @@
end
-instantiation bar :: (sfp) sfp
+instantiation bar :: (bifinite) bifinite
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -139,7 +139,7 @@
end
-instantiation baz :: (sfp) sfp
+instantiation baz :: (bifinite) bifinite
begin
definition emb_baz :: "'a baz \<rightarrow> udom"
--- a/src/HOLCF/ex/Powerdomain_ex.thy Thu Oct 07 13:54:43 2010 -0700
+++ b/src/HOLCF/ex/Powerdomain_ex.thy Fri Oct 08 07:39:50 2010 -0700
@@ -8,7 +8,7 @@
imports HOLCF
begin
-default_sort sfp
+default_sort bifinite
subsection {* Monadic sorting example *}