src/HOL/Set.ML
changeset 1937 e59ff0eb1e91
parent 1920 df683ce7aad8
child 1985 84cf16192e03
     1.1 --- a/src/HOL/Set.ML	Thu Aug 22 12:24:25 1996 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Aug 22 12:24:58 1996 +0200
     1.3 @@ -504,6 +504,11 @@
     1.4  val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
     1.5  		  mem_Collect_eq];
     1.6  
     1.7 +(*Not for Addsimps -- it can cause goals to blow up!*)
     1.8 +goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
     1.9 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.10 +qed "mem_if";
    1.11 +
    1.12  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    1.13  
    1.14  simpset := !simpset addsimps mem_simps