src/CCL/Gfp.thy
changeset 21404 eb85850d3eb7
parent 20140 98acc6d0fab6
child 32153 a0e57fb1b930
     1.1 --- a/src/CCL/Gfp.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/CCL/Gfp.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  gfp :: "['a set=>'a set] => 'a set"    (*greatest fixed point*)
     1.8 +  gfp :: "['a set=>'a set] => 'a set" where -- "greatest fixed point"
     1.9    "gfp(f) == Union({u. u <= f(u)})"
    1.10  
    1.11  (* gfp(f) is the least upper bound of {u. u <= f(u)} *)