src/HOL/TPTP/ATP_Problem_Import.thy
author wenzelm
Sun Jun 30 11:37:34 2013 +0200 (2013-06-30)
changeset 52487 48bc24467008
parent 52470 dedd7952a62c
child 57812 8dc9dc241973
permissions -rw-r--r--
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
     1 (*  Title:      HOL/TPTP/ATP_Problem_Import.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 *)
     4 
     5 header {* ATP Problem Importer *}
     6 
     7 theory ATP_Problem_Import
     8 imports
     9   Complex_Main
    10   TPTP_Interpret
    11   "~~/src/HOL/Library/Refute"
    12 begin
    13 
    14 ML_file "sledgehammer_tactics.ML"
    15 
    16 ML {* Proofterm.proofs := 0 *}
    17 
    18 declare [[show_consts]] (* for Refute *)
    19 declare [[smt_oracle]]
    20 
    21 declare [[unify_search_bound = 60]]
    22 declare [[unify_trace_bound = 60]]
    23 
    24 ML_file "atp_problem_import.ML"
    25 
    26 (*
    27 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
    28           "$TPTP/Problems/PUZ/PUZ107^5.p" *}
    29 *)
    30 
    31 end