| changeset 47765 | 18f37b7aa6a6 |
| parent 47714 | d6683fe037b1 |
| child 47766 | 9f7cdd5fff7c |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 20:08:33 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Apr 25 22:00:33 2012 +0200 @@ -9,7 +9,10 @@ uses ("atp_problem_import.ML") begin +ML {* Proofterm.proofs := 0 *} + declare [[show_consts]] (* for Refute *) +declare [[smt_oracle]] use "atp_problem_import.ML"