--- a/src/ZF/WF.thy Sun Nov 02 16:09:35 2014 +0100 +++ b/src/ZF/WF.thy Sun Nov 02 16:39:54 2014 +0100 @@ -14,7 +14,7 @@ a mess. *) -header{*Well-Founded Recursion*} +section{*Well-Founded Recursion*} theory WF imports Trancl begin