# HG changeset patch
# User paulson
# Date 881832562 -3600
# Node ID b3cff8adc213bd3d5fd21ede64aa38be8534be79
# Parent  f6d019eefa1ed61186ab43dae102304cad949b3f
Tidied proof of finite_subset_induct

diff -r f6d019eefa1e -r b3cff8adc213 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Thu Dec 11 10:28:04 1997 +0100
+++ b/src/HOL/Finite.ML	Thu Dec 11 10:29:22 1997 +0100
@@ -35,21 +35,14 @@
 by (REPEAT (ares_tac prems 1));
 qed "finite_induct";
 
-val major::prems = goal Finite.thy 
-    "[| finite F; \
-\       P({}); \
-\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
-\    |] ==> F <= A --> P(F)";
-by (rtac (major RS finite_induct) 1);
-by (ALLGOALS (blast_tac (claset() addIs prems)));
-val lemma = result();
-
-val prems = goal Finite.thy 
+val major::subs::prems = goal Finite.thy 
     "[| finite F;  F <= A; \
 \       P({}); \
 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
 \    |] ==> P(F)";
-by (blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
+by (rtac (subs RS rev_mp) 1);
+by (rtac (major RS finite_induct) 1);
+by (ALLGOALS (blast_tac (claset() addIs prems)));
 qed "finite_subset_induct";
 
 Addsimps Finites.intrs;