equal
deleted
inserted
replaced
57 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
57 | _$(Const("op -->",_)$_$_) => at(thm RS mp) |
58 | _ => [thm] |
58 | _ => [thm] |
59 in map zero_var_indexes (at thm) end; |
59 in map zero_var_indexes (at thm) end; |
60 |
60 |
61 val atomize_ss = |
61 val atomize_ss = |
62 Simplifier.theory_context @{theory} empty_ss |
62 Simplifier.global_context @{theory} empty_ss |
63 setmksimps (mksimps mksimps_pairs) |
63 setmksimps (mksimps mksimps_pairs) |
64 addsimps [ |
64 addsimps [ |
65 all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
65 all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
66 imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
66 imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *) |
67 imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |
67 imp_conjR, (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *) |