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