# HG changeset patch
# User blanchet
# Date 1286267291 -7200
# Node ID 317010af89727c46729f713370a9913a215f41c9
# Parent  f95834c8bb4d4debff8cdf7ac198112261571604
factor out "Meson_Tactic" from "Meson_Clausify"

diff -r f95834c8bb4d -r 317010af8972 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Oct 04 22:51:53 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Oct 05 10:28:11 2010 +0200
@@ -205,6 +205,7 @@
   Tools/lin_arith.ML \
   Tools/Meson/meson.ML \
   Tools/Meson/meson_clausify.ML \
+  Tools/Meson/meson_tactic.ML \
   Tools/Metis/metis_reconstruct.ML \
   Tools/Metis/metis_translate.ML \
   Tools/Metis/metis_tactics.ML \
diff -r f95834c8bb4d -r 317010af8972 src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Mon Oct 04 22:51:53 2010 +0200
+++ b/src/HOL/Meson.thy	Tue Oct 05 10:28:11 2010 +0200
@@ -11,6 +11,7 @@
 imports Datatype
 uses ("Tools/Meson/meson.ML")
      ("Tools/Meson/meson_clausify.ML")
+     ("Tools/Meson/meson_tactic.ML")
 begin
 
 section {* Negation Normal Form *}
@@ -197,11 +198,12 @@
 
 use "Tools/Meson/meson.ML"
 use "Tools/Meson/meson_clausify.ML"
+use "Tools/Meson/meson_tactic.ML"
 
 setup {*
   Meson_Choices.setup
   #> Meson.setup
-  #> Meson_Clausify.setup
+  #> Meson_Tactic.setup
 *}
 
 end
diff -r f95834c8bb4d -r 317010af8972 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 22:51:53 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
@@ -3,7 +3,6 @@
     Author:     Jasmin Blanchette, TU Muenchen
 
 Transformation of HOL theorems into CNF forms.
-The "meson" proof method for HOL.
 *)
 
 signature MESON_CLAUSIFY =
@@ -16,8 +15,6 @@
   val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
   val cnf_axiom :
     Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
-  val meson_general_tac : Proof.context -> thm list -> int -> tactic
-  val setup: theory -> theory
 end;
 
 structure Meson_Clausify : MESON_CLAUSIFY =
@@ -365,14 +362,4 @@
   end
   handle THM _ => (NONE, [])
 
-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;
diff -r f95834c8bb4d -r 317010af8972 src/HOL/Tools/Meson/meson_tactic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Meson/meson_tactic.ML	Tue Oct 05 10:28:11 2010 +0200
@@ -0,0 +1,29 @@
+(*  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;