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