src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Jul 24 17:52:38 2003 +0200
+++ b/src/HOL/Nat.thy	Thu Jul 24 18:23:00 2003 +0200
@@ -346,7 +346,9 @@
   apply assumption
   done
 
-subsection {* Properties of "less or equal than" *}
+lemmas less_induct = nat_less_induct [rule_format, case_names less]
+
+subsection {* Properties of "less than or equal" *}
 
 text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
 lemma less_Suc_eq_le: "(m < Suc n) = (m <= n)"