Tidied proofs

--- a/src/HOL/Finite.ML	Fri Apr 03 11:20:41 1998 +0200
+++ b/src/HOL/Finite.ML	Fri Apr 03 11:22:51 1998 +0200
@@ -320,11 +320,9 @@
 by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
- by (SELECT_GOAL Safe_tac 1);
- by (rotate_tac ~1 1);
- by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 2);
+by (fast_tac (claset() addss
+	      (simpset() addsimps [subset_insert_iff, finite_subset])) 1);
 qed_spec_mp "card_mono";
 
 goal Finite.thy "!!A B. [| finite A; finite B |]\
@@ -399,23 +397,20 @@
 
 (*Proper subsets*)
 goalw Finite.thy [psubset_def]
-"!!B. finite B ==> !A. A < B --> card(A) < card(B)";
+    "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (Clarify_tac 1);
 by (case_tac "x:A" 1);
 (*1*)
 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-by (rotate_tac ~1 1);
-by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
+by (Clarify_tac 1);
+by (rotate_tac ~3 1);
+by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1);
 by (Blast_tac 1);
 (*2*)
-by (rotate_tac ~1 1);
 by (eres_inst_tac [("P","?a<?b")] notE 1);
-by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
+by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
 by (case_tac "A=F" 1);
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "psubset_card" ;