diff -r 768d3504d7cd -r 12dd5d2e266b Lfp.thy
--- 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