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/Lfp.thy
changeset 3947 eb707467f8c5
parent 1558 9c6ebfab4e05
child 8882 9df44a4f1bf7
equal deleted inserted replaced
3946:34152864655c 3947:eb707467f8c5 
     6 The Knaster-Tarski Theorem
 
     6 The Knaster-Tarski Theorem
 
     7 *)
 
     7 *)
 
     8 
     8 
     9 Lfp = mono + Prod +
 
     9 Lfp = mono + Prod +
 
    10 
    10 
       
    11 global
 
       
    12 
    11 constdefs
 
    13 constdefs
 
    12   lfp :: ['a set=>'a set] => 'a set
 
    14   lfp :: ['a set=>'a set] => 'a set
 
    13   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
 
    15   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
 
    14 
    16 
       
    17 local
 
       
    18 
    15 end
 
    19 end
isabelle