| changeset 27310 | d0229bc6c461 |
| parent 27309 | c74270fd72a8 |
| child 27373 | 5794a0e3e26c |
--- a/src/HOLCF/UpperPD.thy Fri Jun 20 22:51:50 2008 +0200 +++ b/src/HOLCF/UpperPD.thy Fri Jun 20 23:01:09 2008 +0200 @@ -147,7 +147,7 @@ instance apply (intro_classes, unfold approx_upper_pd_def) -apply (simp add: upper_pd.chain_completion_approx) +apply (rule upper_pd.chain_completion_approx) apply (rule upper_pd.lub_completion_approx) apply (rule upper_pd.completion_approx_idem) apply (rule upper_pd.finite_fixes_completion_approx)