equal
deleted
inserted
replaced
13 structure Meson_Tactic : MESON_TACTIC = |
13 structure Meson_Tactic : MESON_TACTIC = |
14 struct |
14 struct |
15 |
15 |
16 fun meson_general_tac ctxt ths = |
16 fun meson_general_tac ctxt ths = |
17 let val ctxt' = put_claset HOL_cs ctxt |
17 let val ctxt' = put_claset HOL_cs ctxt |
18 in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom {if_simps = true} ctxt' false true 0) ths) end |
18 in |
|
19 Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt' |
|
20 false true 0) ths) |
|
21 end |
19 |
22 |
20 val _ = |
23 val _ = |
21 Theory.setup |
24 Theory.setup |
22 (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt => |
25 (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt => |
23 SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) |
26 SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) |