src/HOL/Lfp.thy
changeset 3947 eb707467f8c5
parent 1558 9c6ebfab4e05
child 8882 9df44a4f1bf7
--- a/src/HOL/Lfp.thy	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/Lfp.thy	Mon Oct 20 11:25:39 1997 +0200
@@ -8,8 +8,12 @@
 
 Lfp = mono + Prod +
 
+global
+
 constdefs
   lfp :: ['a set=>'a set] => 'a set
   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
 
+local
+
 end