--- a/src/HOL/Tools/Sledgehammer/meson_tactic.ML Mon Sep 27 09:17:24 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
- Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
- Author: Jasmin Blanchette, TU Muenchen
-
-MESON general tactic and proof method.
-*)
-
-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
-
-fun meson_general_tac ctxt ths =
- let
- val thy = ProofContext.theory_of ctxt
- val ctxt0 = Classical.put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) 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;