--- a/src/HOL/Lfp.thy Mon Nov 27 13:44:56 1995 +0100
+++ b/src/HOL/Lfp.thy Wed Nov 29 16:44:59 1995 +0100
@@ -7,7 +7,7 @@
*)
Lfp = mono + Prod +
-consts lfp :: "['a set=>'a set] => 'a set"
+consts lfp :: ['a set=>'a set] => 'a set
defs
(*least fixed point*)
lfp_def "lfp(f) == Inter({u. f(u) <= u})"