src/HOL/Set.ML
changeset 1937 e59ff0eb1e91
parent 1920 df683ce7aad8
child 1985 84cf16192e03
equal deleted inserted replaced
1936:979e8b4f5fa5 1937:e59ff0eb1e91
   502 
   502 
   503 
   503 
   504 val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
   504 val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
   505 		  mem_Collect_eq];
   505 		  mem_Collect_eq];
   506 
   506 
       
   507 (*Not for Addsimps -- it can cause goals to blow up!*)
       
   508 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
       
   509 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
       
   510 qed "mem_if";
       
   511 
   507 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
   512 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
   508 
   513 
   509 simpset := !simpset addsimps mem_simps
   514 simpset := !simpset addsimps mem_simps
   510                     addcongs [ball_cong,bex_cong]
   515                     addcongs [ball_cong,bex_cong]
   511                     setmksimps (mksimps mksimps_pairs);
   516                     setmksimps (mksimps mksimps_pairs);