--- a/src/HOLCF/ConvexPD.thy Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy Mon May 19 23:49:20 2008 +0200
@@ -206,12 +206,13 @@
subsection {* Approximation *}
-instance convex_pd :: (profinite) approx ..
+instantiation convex_pd :: (profinite) profinite
+begin
-defs (overloaded)
- approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
+definition
+ approx_convex_pd_def: "approx = convex_pd.completion_approx"
-instance convex_pd :: (profinite) profinite
+instance
apply (intro_classes, unfold approx_convex_pd_def)
apply (simp add: convex_pd.chain_completion_approx)
apply (rule convex_pd.lub_completion_approx)
@@ -219,6 +220,8 @@
apply (rule convex_pd.finite_fixes_completion_approx)
done
+end
+
instance convex_pd :: (bifinite) bifinite ..
lemma approx_convex_principal [simp]: