--- a/src/HOL/NatDef.thy Thu Oct 12 18:09:06 2000 +0200 +++ b/src/HOL/NatDef.thy Thu Oct 12 18:38:23 2000 +0200 @@ -8,7 +8,7 @@ Type nat is defined as a set Nat over type ind. *) -NatDef = WF + +NatDef = Wellfounded_Recursion + (** type ind **)