diff -r 0ec63df3ae04 -r ab4328bbff70 Lfp.thy
--- 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*)