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