src/HOLCF/Up.thy
changeset 26407 562a1d615336
parent 26046 1624b3304bb9
child 26962 c8b20f615d6c
     1.1 --- a/src/HOLCF/Up.thy	Wed Mar 26 21:05:58 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Mar 26 22:38:17 2008 +0100
     1.3 @@ -311,13 +311,13 @@
     1.4  
     1.5  subsection {* Lifted cpo is a bifinite domain *}
     1.6  
     1.7 -instance u :: (bifinite_cpo) approx ..
     1.8 +instance u :: (profinite) approx ..
     1.9  
    1.10  defs (overloaded)
    1.11    approx_up_def:
    1.12      "approx \<equiv> \<lambda>n. fup\<cdot>(\<Lambda> x. up\<cdot>(approx n\<cdot>x))"
    1.13  
    1.14 -instance u :: (bifinite_cpo) bifinite
    1.15 +instance u :: (profinite) bifinite
    1.16  proof
    1.17    fix i :: nat and x :: "'a u"
    1.18    show "chain (\<lambda>i. approx i\<cdot>x)"