src/HOL/Set.ML
changeset 5237 aebc63048f2d
parent 5148 74919e8f221c
child 5256 e6983301ce5e
     1.1 --- a/src/HOL/Set.ML	Tue Aug 04 09:22:07 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Aug 04 10:46:44 1998 +0200
     1.3 @@ -649,6 +649,8 @@
     1.4  bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
     1.5  bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
     1.6  
     1.7 +(*Split ifs on either side of the membership relation.
     1.8 +	Not for Addsimps -- can cause goals to blow up!*)
     1.9  bind_thm ("split_if_mem1", 
    1.10      read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
    1.11  bind_thm ("split_if_mem2", 
    1.12 @@ -662,11 +664,6 @@
    1.13  val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.14                   mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
    1.15  
    1.16 -(*Not for Addsimps -- it can cause goals to blow up!*)
    1.17 -Goal "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.18 -by (Simp_tac 1);
    1.19 -qed "mem_if";
    1.20 -
    1.21  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    1.22  
    1.23  simpset_ref() := simpset() addcongs [ball_cong,bex_cong]