src/HOL/TPTP/MaSh_Export_Base.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned proofs;
blanchet@58206
     1
(*  Title:      HOL/TPTP/MaSh_Export_Base.thy
blanchet@58206
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@58206
     3
*)
blanchet@58206
     4
wenzelm@63167
     5
section \<open>MaSh Exporter Base\<close>
blanchet@58206
     6
blanchet@58206
     7
theory MaSh_Export_Base
blanchet@58206
     8
imports Main
blanchet@58206
     9
begin
blanchet@58206
    10
blanchet@58206
    11
ML_file "mash_export.ML"
blanchet@58206
    12
blanchet@58206
    13
sledgehammer_params
blanchet@58206
    14
  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
blanchet@58206
    15
   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
blanchet@58206
    16
blanchet@58206
    17
declare [[sledgehammer_fact_duplicates = true]]
blanchet@58206
    18
declare [[sledgehammer_instantiate_inducts = false]]
blanchet@58206
    19
blanchet@58206
    20
hide_fact (open) HOL.ext
blanchet@58206
    21
wenzelm@63167
    22
ML \<open>
wenzelm@62925
    23
Multithreading.max_threads ()
wenzelm@63167
    24
\<close>
blanchet@58206
    25
wenzelm@63167
    26
ML \<open>
blanchet@58206
    27
open MaSh_Export
wenzelm@63167
    28
\<close>
blanchet@58206
    29
wenzelm@63167
    30
ML \<open>
blanchet@58206
    31
val do_it = false (* switch to "true" to generate the files *)
blanchet@58206
    32
val thys = [@{theory List}]
blanchet@58206
    33
val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
blanchet@58206
    34
val prover = hd provers
blanchet@58206
    35
val range = (1, NONE)
blanchet@58206
    36
val step = 1
blanchet@58206
    37
val max_suggestions = 1024
blanchet@58206
    38
val dir = "List"
blanchet@58206
    39
val prefix = "/tmp/" ^ dir ^ "/"
wenzelm@63167
    40
\<close>
blanchet@58206
    41
blanchet@58206
    42
end