1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 04 18:57:45 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 04 19:01:36 2014 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4    bool * (string option * string option) * Time.time * real * bool * bool
     1.5    * (term, string) atp_step list * thm
     1.6  
     1.7 -val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method]
     1.8 +val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
     1.9  val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
    1.10  val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
    1.11  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 18:57:45 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 19:01:36 2014 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4      Metis_Method of string option * string option |
     2.5      Meson_Method |
     2.6      SMT2_Method |
     2.7 +    SATx_Method |
     2.8      Blast_Method |
     2.9      Simp_Method |
    2.10      Simp_Size_Method |
    2.11 @@ -51,6 +52,7 @@
    2.12    Metis_Method of string option * string option |
    2.13    Meson_Method |
    2.14    SMT2_Method |
    2.15 +  SATx_Method |
    2.16    Blast_Method |
    2.17    Simp_Method |
    2.18    Simp_Size_Method |
    2.19 @@ -77,6 +79,7 @@
    2.20      "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
    2.21    | Meson_Method => "meson"
    2.22    | SMT2_Method => "smt2"
    2.23 +  | SATx_Method => "satx"
    2.24    | Blast_Method => "blast"
    2.25    | Simp_Method => "simp"
    2.26    | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
    2.27 @@ -105,7 +108,8 @@
    2.28      | _ =>
    2.29        Method.insert_tac global_facts THEN'
    2.30        (case meth of
    2.31 -        Blast_Method => blast_tac ctxt
    2.32 +        SATx_Method => SAT.satx_tac ctxt
    2.33 +      | Blast_Method => blast_tac ctxt
    2.34        | Simp_Method => Simplifier.asm_full_simp_tac ctxt
    2.35        | Simp_Size_Method =>
    2.36          Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)