src/HOL/TPTP/MaSh_Export_Base.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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