--- a/Lfp.thy Fri Aug 19 11:02:45 1994 +0200 +++ b/Lfp.thy Fri Aug 19 11:10:56 1994 +0200 @@ -6,7 +6,7 @@ The Knaster-Tarski Theorem *) -Lfp = Sum + +Lfp = mono + consts lfp :: "['a set=>'a set] => 'a set" rules (*least fixed point*)