--- a/src/HOL/Finite_Set.thy Wed Nov 27 17:25:41 2002 +0100
+++ b/src/HOL/Finite_Set.thy Thu Nov 28 10:50:42 2002 +0100
@@ -273,6 +273,22 @@
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
by (induct k) (simp_all add: atMost_Suc)
+lemma finite_greaterThanLessThan [iff]:
+ fixes l :: nat shows "finite {)l..u(}"
+by (simp add: greaterThanLessThan_def)
+
+lemma finite_atLeastLessThan [iff]:
+ fixes l :: nat shows "finite {l..u(}"
+by (simp add: atLeastLessThan_def)
+
+lemma finite_greaterThanAtMost [iff]:
+ fixes l :: nat shows "finite {)l..u}"
+by (simp add: greaterThanAtMost_def)
+
+lemma finite_atLeastAtMost [iff]:
+ fixes l :: nat shows "finite {l..u}"
+by (simp add: atLeastAtMost_def)
+
lemma bounded_nat_set_is_finite:
"(ALL i:N. i < (n::nat)) ==> finite N"
-- {* A bounded set of natural numbers is finite. *}