# HG changeset patch
# User wenzelm
# Date 1007595580 -3600
# Node ID 6766aa05e4eb394660c5eb8b7c904641de00aa37
# Parent  2298d5b8e5304d164972d8498355aeb48eb1d7c7
less_induct, wf_induct_rule;

diff -r 2298d5b8e530 -r 6766aa05e4eb src/HOL/PreList.thy
--- 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 *)