--- 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"