src/HOL/WF.thy

--- a/src/HOL/WF.thy	Mon Oct 20 11:22:29 1997 +0200
+++ b/src/HOL/WF.thy	Mon Oct 20 11:25:39 1997 +0200
@@ -8,6 +8,8 @@
 
 WF = Trancl +
 
+global
+
 constdefs
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
@@ -28,4 +30,6 @@
   "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
                             r x)  x)"
 
+local
+
 end