author | blanchet |
Fri, 27 Apr 2012 12:16:10 +0200 | |
changeset 47785 | d27bb852c430 |
parent 47770 | 53e30966b4b6 |
child 47788 | 44b33c1e702e |
permissions | -rw-r--r-- |
(* Title: HOL/TPTP/ATP_Problem_Import.thy Author: Jasmin Blanchette, TU Muenchen *) header {* ATP Problem Importer *} theory ATP_Problem_Import imports Complex_Main TPTP_Interpret uses "~~/src/HOL/ex/sledgehammer_tactics.ML" "atp_problem_import.ML" begin ML {* Proofterm.proofs := 0 *} declare [[show_consts]] (* for Refute *) declare [[smt_oracle]] (* ML {* ATP_Problem_Import.isabelle_tptp_file 100 "$TPTP/Problems/PUZ/PUZ107^5.p" *} *) end