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