less_induct, wf_induct_rule;
authorwenzelm
Thu Dec 06 00:39:40 2001 +0100 (2001-12-06)
changeset 123976766aa05e4eb
parent 12396 2298d5b8e530
child 12398 9c27f28c8f5a
less_induct, wf_induct_rule;
src/HOL/PreList.thy
     1.1 --- a/src/HOL/PreList.thy	Thu Dec 06 00:38:55 2001 +0100
     1.2 +++ b/src/HOL/PreList.thy	Thu Dec 06 00:39:40 2001 +0100
     1.3 @@ -14,8 +14,11 @@
     1.4  (*belongs to theory Divides*)
     1.5  declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
     1.6  
     1.7 +(*belongs to theory Nat*)
     1.8 +lemmas less_induct = nat_less_induct [rule_format, case_names less]
     1.9 +
    1.10  (*belongs to theory Wellfounded_Recursion*)
    1.11 -declare wf_induct [induct set: wf]
    1.12 +lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
    1.13  
    1.14  
    1.15  (* generic summation indexed over nat *)