src/HOL/TPTP/ATP_Problem_Import.thy
changeset 47790 2e1636e45770
parent 47788 44b33c1e702e
child 47794 4ad62c5f9f88
equal deleted inserted replaced
47789:71a526ee569a 47790:2e1636e45770
     1 (*  Title:      HOL/TPTP/ATP_Problem_Import.thy
     1 (*  Title:      HOL/TPTP/ATP_Problem_Import.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 *)
     3 *)
     4 
     4 
     5 header {* ATP Problem Importer *}
     5 header {* ATP Problem Importer *}
     6 
       
     7 theory ATP_Problem_Import
     6 theory ATP_Problem_Import
     8 imports Complex_Main TPTP_Interpret
     7 imports Complex_Main TPTP_Interpret
     9 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
     8 uses "sledgehammer_tactics.ML"
    10      "atp_problem_import.ML"
     9      "atp_problem_import.ML"
    11 begin
    10 begin
    12 
    11 
    13 ML {* Proofterm.proofs := 0 *}
    12 ML {* Proofterm.proofs := 0 *}
    14 
    13