src/HOL/Tools/Meson/meson_clausify.ML
changeset 39948 317010af8972
parent 39941 02fcd9cd1eac
child 39949 186a3b447e0b
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Mon Oct 04 22:51:53 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
     1.3 @@ -3,7 +3,6 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5  
     1.6  Transformation of HOL theorems into CNF forms.
     1.7 -The "meson" proof method for HOL.
     1.8  *)
     1.9  
    1.10  signature MESON_CLAUSIFY =
    1.11 @@ -16,8 +15,6 @@
    1.12    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    1.13    val cnf_axiom :
    1.14      Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
    1.15 -  val meson_general_tac : Proof.context -> thm list -> int -> tactic
    1.16 -  val setup: theory -> theory
    1.17  end;
    1.18  
    1.19  structure Meson_Clausify : MESON_CLAUSIFY =
    1.20 @@ -365,14 +362,4 @@
    1.21    end
    1.22    handle THM _ => (NONE, [])
    1.23  
    1.24 -fun meson_general_tac ctxt ths =
    1.25 -  let val ctxt = Classical.put_claset HOL_cs ctxt in
    1.26 -    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
    1.27 -  end
    1.28 -
    1.29 -val setup =
    1.30 -  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    1.31 -     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    1.32 -     "MESON resolution proof procedure"
    1.33 -
    1.34  end;