# HG changeset patch
# User oheimb
# Date 964194389 -7200
# Node ID effc8d44c89c763910e7d5846fb458c164dbd2ea
# Parent  0ee9b281915564c947ed24e249a49deffc7b5947
removed weaker variant of subset_insert_iff

diff -r 0ee9b2819155 -r effc8d44c89c src/HOL/Finite.ML
--- 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";
 
 
diff -r 0ee9b2819155 -r effc8d44c89c src/HOL/equalities.ML
--- 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";