--- a/src/HOLCF/LowerPD.thy Fri Jun 20 22:41:41 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Fri Jun 20 22:51:50 2008 +0200
@@ -284,7 +284,7 @@
lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
apply (rule iffI)
- apply (rule bifinite_less_ext)
+ apply (rule profinite_less_ext)
apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -331,7 +331,7 @@
done
lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
-unfolding bifinite_compact_iff by simp
+unfolding profinite_compact_iff by simp
lemma compact_lower_plus [simp]:
"\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"