--- a/src/HOL/Divides.thy Thu Jul 24 17:52:38 2003 +0200
+++ b/src/HOL/Divides.thy Thu Jul 24 18:23:00 2003 +0200
@@ -44,6 +44,8 @@
use "Divides_lemmas.ML"
+declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]
+
lemma split_div:
"P(n div k :: nat) =
((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
--- 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)"