Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Meson/meson_tactic.ML
author wenzelm
Mon, 21 Mar 2016 20:22:07 +0100
changeset 62681 45b8dd2d3827
parent 58817 4cd778c91fdc
child 67149 e61557884799
permissions -rw-r--r--
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;

(*  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
end;

structure Meson_Tactic : MESON_TACTIC =
struct

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

val _ =
  Theory.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;
isabelle