equal
deleted
inserted
replaced
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() := |
48 simpset_ref() := |
49 simpset() setmksimps (map mk_eq o ZF_atomize o forall_elim_vars_safe) |
49 simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) |
50 addcongs [if_weak_cong] |
50 addcongs [if_weak_cong] |
51 addsplits [split_if] |
51 addsplits [split_if] |
52 setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); |
52 setSolver (mk_solver "types" (fn prems => TCSET' (fn tcset => type_solver_tac tcset prems))); |
53 |
53 |
54 |
54 |