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
     1 (*  Title:      HOL/TPTP/MaSh_Export_Base.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 *)
     4 
     5 section \<open>MaSh Exporter Base\<close>
     6 
     7 theory MaSh_Export_Base
     8 imports Main
     9 begin
    10 
    11 ML_file "mash_export.ML"
    12 
    13 sledgehammer_params
    14   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
    15    lam_trans = lifting, timeout = 2, dont_preplay, minimize]
    16 
    17 declare [[sledgehammer_fact_duplicates = true]]
    18 declare [[sledgehammer_instantiate_inducts = false]]
    19 
    20 hide_fact (open) HOL.ext
    21 
    22 ML \<open>
    23 Multithreading.max_threads ()
    24 \<close>
    25 
    26 ML \<open>
    27 open MaSh_Export
    28 \<close>
    29 
    30 ML \<open>
    31 val do_it = false (* switch to "true" to generate the files *)
    32 val thys = [@{theory List}]
    33 val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
    34 val prover = hd provers
    35 val range = (1, NONE)
    36 val step = 1
    37 val max_suggestions = 1024
    38 val dir = "List"
    39 val prefix = "/tmp/" ^ dir ^ "/"
    40 \<close>
    41 
    42 end