src/HOL/HOLCF/Library/Defl_Bifinite.thy
changeset 41286 3d7685a4a5ff
parent 40774 0437dbc127b3
child 41287 029a6fc1bfb8
     1.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 04:06:02 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Dec 19 05:15:31 2010 -0800
     1.3 @@ -609,6 +609,9 @@
     1.4  
     1.5  subsection {* Algebraic deflations are a bifinite domain *}
     1.6  
     1.7 +instance defl :: bifinite
     1.8 +  by default (fast intro!: defl_approx)
     1.9 +
    1.10  instantiation defl :: liftdomain
    1.11  begin
    1.12