--- a/src/HOL/Set.ML Thu Aug 22 12:24:25 1996 +0200
+++ b/src/HOL/Set.ML Thu Aug 22 12:24:58 1996 +0200
@@ -504,6 +504,11 @@
val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_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))";
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed "mem_if";
+
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
simpset := !simpset addsimps mem_simps