--- a/src/ZF/WF.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/WF.thy Fri Jun 17 16:12:49 2005 +0200 @@ -17,7 +17,7 @@ header{*Well-Founded Recursion*} -theory WF = Trancl: +theory WF imports Trancl begin constdefs wf :: "i=>o"