src/ZF/simpdata.ML
changeset 12209 09bc6f8456b9
parent 12199 8213fd95acb5
child 12484 7ad150f5fc10
equal deleted inserted replaced
12208:5efe7b6874fd 12209:09bc6f8456b9
    43    ("op -",     [DiffD1,DiffD2]),
    43    ("op -",     [DiffD1,DiffD2]),
    44    ("op Int",   [IntD1,IntD2])];
    44    ("op Int",   [IntD1,IntD2])];
    45 
    45 
    46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    46 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
    47 
    47 
    48 simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    48 simpset_ref() :=
    49                            addcongs [if_weak_cong]
    49   simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
    50 		           addsplits [split_if]
    50   addcongs [if_weak_cong]
    51                            setSolver (mk_solver "types" Type_solver_tac);
    51   addsplits [split_if]
       
    52   setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems)));
       
    53 
    52 
    54 
    53 (** Splitting IFs in the assumptions **)
    55 (** Splitting IFs in the assumptions **)
    54 
    56 
    55 Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
    57 Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
    56 by (Simp_tac 1); 
    58 by (Simp_tac 1);