--- 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 \
--- 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
--- 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;
--- /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;