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