equal
deleted
inserted
replaced
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); |