--- 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]