--- a/src/HOL/Finite.ML Fri Jul 21 17:41:59 2000 +0200
+++ b/src/HOL/Finite.ML Fri Jul 21 17:46:29 2000 +0200
@@ -41,10 +41,10 @@
(*Every subset of a finite set is finite*)
Goal "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","A")] (insert_Diff RS subst) 2);
-by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (simp_tac (simpset() addsimps [subset_insert_iff])));
+by Safe_tac;
+ by (eres_inst_tac [("t","A")] (insert_Diff RS subst) 1);
+ by (ALLGOALS Blast_tac);
val lemma = result();
Goal "[| A<=B; finite B |] ==> finite A";
@@ -784,10 +784,10 @@
by (simp_tac (simpset() addsimps prems) 1);
by (subgoal_tac
"ALL C. C <= B --> (ALL x:C. f x = g x) --> setsum f C = setsum g C" 1);
-by (asm_simp_tac (simpset() addsimps prems) 1);
+ by (asm_simp_tac (simpset() addsimps prems) 1);
by (etac finite_induct 1);
by (Simp_tac 1);
- by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1);
+by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1);
by (Clarify_tac 1);
by (subgoal_tac "finite C" 1);
by (blast_tac (claset() addDs [rotate_prems 1 finite_subset]) 2);
@@ -796,7 +796,7 @@
by (etac ssubst 1);
by (dtac spec 1);
by (mp_tac 1);
- by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1);
+by (asm_full_simp_tac (simpset() addsimps Ball_def::prems) 1);
qed "setsum_cong";
--- a/src/HOL/equalities.ML Fri Jul 21 17:41:59 2000 +0200
+++ b/src/HOL/equalities.ML Fri Jul 21 17:46:29 2000 +0200
@@ -354,10 +354,6 @@
by (blast_tac (claset() addSEs [equalityCE]) 1);
qed "subset_Un_eq";
-Goal "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
-by (Blast_tac 1);
-qed "subset_insert_iff";
-
Goal "(A Un B = {}) = (A = {} & B = {})";
by (blast_tac (claset() addEs [equalityCE]) 1);
qed "Un_empty";