src/CCL/Gfp.thy
changeset 17456 bcf7544875b2
parent 1474 3f7d67927fe2
child 20140 98acc6d0fab6
equal deleted inserted replaced
17455:151e76f0e3c7 17456:bcf7544875b2
     1 (*  Title:      HOL/gfp.thy
     1 (*  Title:      CCL/Gfp.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
       
     6 Greatest fixed points
       
     7 *)
     5 *)
     8 
     6 
     9 Gfp = Lfp +
     7 header {* Greatest fixed points *}
    10 consts gfp :: "['a set=>'a set] => 'a set"
     8 
    11 rules
     9 theory Gfp
    12  (*greatest fixed point*)
    10 imports Lfp
    13  gfp_def "gfp(f) == Union({u. u <= f(u)})"
    11 begin
       
    12 
       
    13 constdefs
       
    14   gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
       
    15   "gfp(f) == Union({u. u <= f(u)})"
       
    16 
       
    17 ML {* use_legacy_bindings (the_context ()) *}
       
    18 
    14 end
    19 end