--- a/Lfp.thy Thu Nov 24 20:11:40 1994 +0100 +++ b/Lfp.thy Thu Nov 24 20:31:09 1994 +0100 @@ -8,7 +8,7 @@ Lfp = mono + consts lfp :: "['a set=>'a set] => 'a set" -rules +defs (*least fixed point*) lfp_def "lfp(f) == Inter({u. f(u) <= u})" end