# HG changeset patch
# User paulson
# Date 840709498 -7200
# Node ID e59ff0eb1e91a6c4a14c1ed59e39f5d2cbe7670a
# Parent  979e8b4f5fa5f63118a6706837c498ea52e0d1cb
Proved mem_if

diff -r 979e8b4f5fa5 -r e59ff0eb1e91 src/HOL/Set.ML
--- 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