# HG changeset patch
# User paulson
# Date 902220404 -7200
# Node ID aebc63048f2dc08b8389c8f9d736df054f95dc6e
# Parent  0cec0b591d4ce9f98c8941fa8a6a1aede5bcbc07
Deleted the redundant rule mem_if

diff -r 0cec0b591d4c -r aebc63048f2d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Aug 04 09:22:07 1998 +0200
+++ b/src/HOL/Set.ML	Tue Aug 04 10:46:44 1998 +0200
@@ -649,6 +649,8 @@
 bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
 bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
 
+(*Split ifs on either side of the membership relation.
+	Not for Addsimps -- can cause goals to blow up!*)
 bind_thm ("split_if_mem1", 
     read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
 bind_thm ("split_if_mem2", 
@@ -662,11 +664,6 @@
 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
                  mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
 
-(*Not for Addsimps -- it can cause goals to blow up!*)
-Goal "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
-by (Simp_tac 1);
-qed "mem_if";
-
 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
 
 simpset_ref() := simpset() addcongs [ball_cong,bex_cong]