src/HOLCF/UpperPD.thy
changeset 26962 c8b20f615d6c
parent 26927 8684b5240f11
child 27267 5ebfb7f25ebb
     1.1 --- a/src/HOLCF/UpperPD.thy	Sun May 18 17:04:48 2008 +0200
     1.2 +++ b/src/HOLCF/UpperPD.thy	Mon May 19 23:49:20 2008 +0200
     1.3 @@ -156,12 +156,13 @@
     1.4  
     1.5  subsection {* Approximation *}
     1.6  
     1.7 -instance upper_pd :: (profinite) approx ..
     1.8 +instantiation upper_pd :: (profinite) profinite
     1.9 +begin
    1.10  
    1.11 -defs (overloaded)
    1.12 -  approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
    1.13 +definition
    1.14 +  approx_upper_pd_def: "approx = upper_pd.completion_approx"
    1.15  
    1.16 -instance upper_pd :: (profinite) profinite
    1.17 +instance
    1.18  apply (intro_classes, unfold approx_upper_pd_def)
    1.19  apply (simp add: upper_pd.chain_completion_approx)
    1.20  apply (rule upper_pd.lub_completion_approx)
    1.21 @@ -169,6 +170,8 @@
    1.22  apply (rule upper_pd.finite_fixes_completion_approx)
    1.23  done
    1.24  
    1.25 +end
    1.26 +
    1.27  instance upper_pd :: (bifinite) bifinite ..
    1.28  
    1.29  lemma approx_upper_principal [simp]: