src/HOL/Tools/Meson/meson_tactic.ML

proper Proof.context for classical tactics;
reduced claset to snapshot of classical context;
discontinued clasimpset;

(*  Title:      HOL/Tools/Meson/meson_tactic.ML
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    Author:     Jasmin Blanchette, TU Muenchen

The "meson" proof method for HOL.
*)

signature MESON_TACTIC =
sig
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
  val setup: theory -> theory
end;

structure Meson_Tactic : MESON_TACTIC =
struct

open Meson_Clausify

fun meson_general_tac ctxt ths =
  let val ctxt' = put_claset HOL_cs ctxt
  in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end

val setup =
  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
     "MESON resolution proof procedure"

end;