--- a/src/HOL/PreList.thy Thu Dec 06 00:38:55 2001 +0100
+++ b/src/HOL/PreList.thy Thu Dec 06 00:39:40 2001 +0100
@@ -14,8 +14,11 @@
(*belongs to theory Divides*)
declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]
+(*belongs to theory Nat*)
+lemmas less_induct = nat_less_induct [rule_format, case_names less]
+
(*belongs to theory Wellfounded_Recursion*)
-declare wf_induct [induct set: wf]
+lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
(* generic summation indexed over nat *)