src/HOL/Lfp.thy

--- a/src/HOL/Lfp.thy	Wed Mar 06 14:19:39 1996 +0100
+++ b/src/HOL/Lfp.thy	Fri Mar 08 13:11:09 1996 +0100
@@ -7,8 +7,9 @@
 *)
 
 Lfp = mono + Prod +
-consts lfp :: ['a set=>'a set] => 'a set
-defs
- (*least fixed point*)
- lfp_def "lfp(f) == Inter({u. f(u) <= u})"
+
+constdefs
+  lfp :: ['a set=>'a set] => 'a set
+  "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
+
 end