# HG changeset patch
# User paulson
# Date 843642858 -7200
# Node ID 909153d8318f1fea8998dbea0f5e813ec29867f3
# Parent  aa25f20c5d8b6f93e74a8a66af5c0e6ebcc57612
Rationalized the rewriting of membership for {} and insert
by deleting the redundant theorems in_empty and in_insert

diff -r aa25f20c5d8b -r 909153d8318f src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Sep 25 11:10:31 1996 +0200
+++ b/src/HOL/Set.ML	Wed Sep 25 11:14:18 1996 +0200
@@ -501,8 +501,8 @@
 (*** Set reasoning tools ***)
 
 
-val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
-		  mem_Collect_eq];
+val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
+		 mem_Collect_eq];
 
 (*Not for Addsimps -- it can cause goals to blow up!*)
 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
diff -r aa25f20c5d8b -r 909153d8318f src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Sep 25 11:10:31 1996 +0200
+++ b/src/HOL/equalities.ML	Wed Sep 25 11:14:18 1996 +0200
@@ -22,18 +22,6 @@
 qed "subset_empty";
 Addsimps [subset_empty];
 
-section ":";
-
-goal Set.thy "x ~: {}";
-by (Fast_tac 1);
-qed "in_empty";
-Addsimps[in_empty];
-
-goal Set.thy "x : insert y A = (x=y | x:A)";
-by (Fast_tac 1);
-qed "in_insert";
-Addsimps[in_insert];
-
 section "insert";
 
 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)