src/ZF/WF.thy

--- a/src/ZF/WF.thy	Sun Jul 14 15:14:43 2002 +0200
+++ b/src/ZF/WF.thy	Sun Jul 14 19:59:55 2002 +0200
@@ -17,7 +17,7 @@
 
 header{*Well-Founded Recursion*}
 
-theory WF = Trancl + mono + equalities:
+theory WF = Trancl:
 
 constdefs
   wf           :: "i=>o"