--- 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"