--- a/src/ZF/Constructible/WFrec.thy Fri Jul 05 17:48:05 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Fri Jul 05 18:33:50 2002 +0200 @@ -1,3 +1,5 @@ +header{*Relativized Well-Founded Recursion*} + theory WFrec = Wellorderings: