# HG changeset patch
# User chaieb
# Date 1251304472 -3600
# Node ID 8d1263a00392f26cc0c1028b4ac3e3dd0d8d12e3
# Parent  1899b8c47961c864e2369e20f475d28a05e66df0
removed unused theorem finite_Atleast_Atmost

diff -r 1899b8c47961 -r 8d1263a00392 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Aug 24 09:49:50 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Wed Aug 26 17:34:32 2009 +0100
@@ -3926,14 +3926,6 @@
   shows "finite s \<and> card s \<le> card t"
   by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono)
 
-lemma finite_Atleast_Atmost[simp]: "finite {f x |x. x\<in> {(i::'a::finite_intvl_succ) .. j}}"
-proof-
-  have eq: "{f x |x. x\<in> {i .. j}} = f ` {i .. j}" by auto
-  show ?thesis unfolding eq
-    apply (rule finite_imageI)
-    apply (rule finite_intvl)
-    done
-qed
 
 lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
 proof-