equal
deleted
inserted
replaced
662 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, |
662 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, |
663 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]; |
663 mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]; |
664 |
664 |
665 (*Not for Addsimps -- it can cause goals to blow up!*) |
665 (*Not for Addsimps -- it can cause goals to blow up!*) |
666 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; |
666 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))"; |
667 by (simp_tac (simpset() addsplits [expand_if]) 1); |
667 by (Simp_tac 1); |
668 qed "mem_if"; |
668 qed "mem_if"; |
669 |
669 |
670 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; |
670 val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; |
671 |
671 |
672 simpset_ref() := simpset() addcongs [ball_cong,bex_cong] |
672 simpset_ref() := simpset() addcongs [ball_cong,bex_cong] |