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