| changeset 52470 | dedd7952a62c |
| parent 49985 | 5b4b0e4e5205 |
| child 52487 | 48bc24467008 |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Thu Jun 27 20:09:39 2013 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Thu Jun 27 23:17:26 2013 +0200 @@ -13,7 +13,7 @@ ML_file "sledgehammer_tactics.ML" -ML {* Proofterm.proofs := 0 *} +declare [[proofs = 0]] declare [[show_consts]] (* for Refute *) declare [[smt_oracle]]