# HG changeset patch
# User oheimb
# Date 963584857 -7200
# Node ID fcf7f29a34475785e832575b4ad9d9a3986a0dfc
# Parent  58bd51302b2123b6e8ef69f515eccc62708f861c
re-added subset_empty to simpset

diff -r 58bd51302b21 -r fcf7f29a3447 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jul 14 14:51:02 2000 +0200
+++ b/src/HOL/Finite.ML	Fri Jul 14 16:27:37 2000 +0200
@@ -41,7 +41,7 @@
 (*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 (simpset() addsimps [subset_empty]) 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);
@@ -366,7 +366,7 @@
 
 Goal "finite B ==> ALL A. A <= B --> card B <= card A --> A = B";
 by (etac finite_induct 1);
- by (simp_tac (simpset() addsimps [subset_empty]) 1);
+ by (Simp_tac 1);
 by (Clarify_tac 1);
 by (subgoal_tac "finite A & A-{x} <= F" 1);
  by (blast_tac (claset() addIs [finite_subset]) 2); 
@@ -780,7 +780,7 @@
     "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 (etac finite_induct 1);
- by (simp_tac (simpset() addsimps [subset_empty]) 1);
+ by (Simp_tac 1);
  by (asm_simp_tac (simpset() addsimps subset_insert_iff::prems) 1); 
 by (Clarify_tac 1); 
 by (subgoal_tac "finite C" 1);
@@ -857,8 +857,7 @@
 by (etac finite_induct 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong] 
-                             addsimps [subset_empty, card_s_0_eq_empty, 
-				       choose_deconstruct])));
+                             addsimps [card_s_0_eq_empty,choose_deconstruct])));
 by (stac card_Un_disjoint 1);
    by (force_tac (claset(), simpset() addsimps [constr_bij]) 4);
   by (Force_tac 3);
diff -r 58bd51302b21 -r fcf7f29a3447 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Jul 14 14:51:02 2000 +0200
+++ b/src/HOL/Set.ML	Fri Jul 14 16:27:37 2000 +0200
@@ -204,6 +204,8 @@
 by (rtac subset_refl 1);
 qed "equalityD2";
 
+(*Be careful when adding this to the claset as subset_empty is in the simpset:
+  A={} goes to {}<=A and A<={} and then back to A={} !*)
 val prems = Goal
     "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);
diff -r 58bd51302b21 -r fcf7f29a3447 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jul 14 14:51:02 2000 +0200
+++ b/src/HOL/equalities.ML	Fri Jul 14 16:27:37 2000 +0200
@@ -18,11 +18,10 @@
 qed "Collect_const";
 Addsimps [Collect_const];
 
-(*If added as a simprule it can cause looping when equalityE is also present:
-  A={} goes to {}<=A and A<={} and then back to A={} !*)
 Goal "(A <= {}) = (A = {})";
 by (Blast_tac 1);
 qed "subset_empty";
+Addsimps[subset_empty];
 
 Goalw [psubset_def] "~ (A < {})";
 by (Blast_tac 1);