# HG changeset patch
# User paulson
# Date 880561654 -3600
# Node ID af2a2cd9fa512e592f7e630e362661fe02dadf0a
# Parent  c872cc541db2ebb2fa9ba638f7c24c9a19d2fd32
Tidying

diff -r c872cc541db2 -r af2a2cd9fa51 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Nov 26 17:26:12 1997 +0100
+++ b/src/HOL/Finite.ML	Wed Nov 26 17:27:34 1997 +0100
@@ -63,20 +63,23 @@
 qed "finite_UnI";
 
 (*Every subset of a finite set is finite*)
-val [subs,fin] = goal Finite.thy "[| A<=B;  finite B |] ==> finite A";
-by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
-            rtac mp, etac spec,
-            rtac subs]);
-by (rtac (fin RS finite_induct) 1);
-by (simp_tac (simpset() addsimps [subset_Un_eq]) 1);
+goal Finite.thy "!!B. finite B ==> ALL A. A<=B --> finite A";
+by (etac finite_induct 1);
+by (Simp_tac 1);
 by (safe_tac (claset() addSDs [subset_insert_iff RS iffD1]));
-by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
+by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 2);
 by (ALLGOALS Asm_simp_tac);
+val lemma = result();
+
+goal Finite.thy "!!A. [| A<=B;  finite B |] ==> finite A";
+bd lemma 1;
+by (Blast_tac 1);
 qed "finite_subset";
 
 goal Finite.thy "finite(F Un G) = (finite F & finite G)";
-by (blast_tac (claset() addIs [finite_UnI] addDs
-                [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
+by (blast_tac (claset() 
+	         addIs [read_instantiate [("B", "?AA Un ?BB")] finite_subset, 
+			finite_UnI]) 1);
 qed "finite_Un";
 AddIffs[finite_Un];
 
@@ -207,7 +210,7 @@
 
 section "Finite cardinality -- 'card'";
 
-goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
+goal Set.thy "{f i |i. (P i | i=n)} = insert (f n) {f i|i. P i}";
 by (Blast_tac 1);
 val Collect_conv_insert = result();