new finiteness theorems

--- a/src/HOL/UNITY/LessThan.ML	Sun Jun 13 13:54:34 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Sun Jun 13 13:54:56 1999 +0200
@@ -28,6 +28,12 @@
 by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
 qed "lessThan_Suc_atMost";
 
+Goal "finite (lessThan k)";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
+by Auto_tac;
+qed "finite_lessThan";
+
 Goal "(UN m. lessThan m) = UNIV";
 by (Blast_tac 1);
 qed "UN_lessThan_UNIV";
@@ -124,6 +130,12 @@
 by (Blast_tac 1);
 qed "atMost_Suc";
 
+Goal "finite (atMost k)";
+by (induct_tac "k" 1);
+by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
+by Auto_tac;
+qed "finite_atMost";
+
 Goal "(UN m. atMost m) = UNIV";
 by (Blast_tac 1);
 qed "UN_atMost_UNIV";