author | blanchet |
Wed, 25 Apr 2012 22:00:33 +0200 | |
changeset 47765 | 18f37b7aa6a6 |
parent 47714 | d6683fe037b1 |
child 47766 | 9f7cdd5fff7c |
permissions | -rw-r--r-- |
46324 | 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 |
|
47557
32f35b3d9e42
started integrating Nik's parser into TPTP command-line tools
blanchet
parents:
46324
diff
changeset
|
8 |
imports Complex_Main TPTP_Interpret |
46324 | 9 |
uses ("atp_problem_import.ML") |
10 |
begin |
|
11 |
||
47765 | 12 |
ML {* Proofterm.proofs := 0 *} |
13 |
||
47670 | 14 |
declare [[show_consts]] (* for Refute *) |
47765 | 15 |
declare [[smt_oracle]] |
47670 | 16 |
|
46324 | 17 |
use "atp_problem_import.ML" |
18 |
||
19 |
end |