Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Library/Defl_Bifinite.thy
changeset 41286 3d7685a4a5ff
parent 40774 0437dbc127b3
child 41287 029a6fc1bfb8
equal deleted inserted replaced
41285:efd23c1d9886 41286:3d7685a4a5ff 
   607     done
 
   607     done
 
   608 qed
 
   608 qed
 
   609 
   609 
   610 subsection {* Algebraic deflations are a bifinite domain *}
 
   610 subsection {* Algebraic deflations are a bifinite domain *}
 
   611 
   611 
       
   612 instance defl :: bifinite
 
       
   613   by default (fast intro!: defl_approx)
 
       
   614 
   612 instantiation defl :: liftdomain
 
   615 instantiation defl :: liftdomain
 
   613 begin
 
   616 begin
 
   614 
   617 
   615 definition
 
   618 definition
 
   616   "emb = udom_emb defl_approx"
 
   619   "emb = udom_emb defl_approx"
isabelle