src/HOL/Gfp.thy
changeset 3947 eb707467f8c5
parent 1558 9c6ebfab4e05
child 8882 9df44a4f1bf7
     1.1 --- a/src/HOL/Gfp.thy	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/Gfp.thy	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -8,8 +8,12 @@
     1.4  
     1.5  Gfp = Lfp +
     1.6  
     1.7 +global
     1.8 +
     1.9  constdefs
    1.10    gfp :: ['a set=>'a set] => 'a set
    1.11    "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
    1.12  
    1.13 +local
    1.14 +
    1.15  end