--- a/src/ZF/WF.thy Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/WF.thy Fri Jan 03 15:01:55 1997 +0100
@@ -6,7 +6,7 @@
Well-founded Recursion
*)
-WF = Trancl + "mono" + "equalities" +
+WF = Trancl + mono + equalities +
consts
wf :: i=>o
wf_on :: [i,i]=>o ("wf[_]'(_')")