src/HOL/Tools/Meson/meson_tactic.ML

+(*  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 = Classical.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;