# HG changeset patch
# User oheimb
# Date 949064853 -3600
# Node ID 649c46adfccccfe29ced679a9bcdc4f726682532
# Parent  dab09e1ad59447d5bcf64506219dee8553e9e3d8
added finite_range_imageI

diff -r dab09e1ad594 -r 649c46adfccc src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jan 28 12:12:06 2000 +0100
+++ b/src/HOL/Finite.ML	Fri Jan 28 14:07:33 2000 +0100
@@ -85,6 +85,11 @@
 by (Asm_simp_tac 1);
 qed "finite_imageI";
 
+Goal "finite (range g) ==> finite (range (%x. f (g x)))";
+by (Simp_tac 1);
+by (etac finite_imageI 1);
+qed "finite_range_imageI";
+
 val major::prems = Goal 
     "[| finite c;  finite b;                                  \
 \       P(b);                                                   \