# HG changeset patch
# User paulson
# Date 1059063780 -7200
# Node ID a4fc8b1af5e7473ac774ec3bd699273146e13ac6
# Parent  398bc4a885d6c11feb93ae940bb415c239ad000d
declarations moved from PreList.thy

diff -r 398bc4a885d6 -r a4fc8b1af5e7 src/HOL/Divides.thy
--- 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)))"
diff -r 398bc4a885d6 -r a4fc8b1af5e7 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)"