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