| changeset 52487 | 48bc24467008 |
| parent 52470 | dedd7952a62c |
| child 57812 | 8dc9dc241973 |
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Sun Jun 30 11:30:16 2013 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sun Jun 30 11:37:34 2013 +0200 @@ -13,7 +13,7 @@ ML_file "sledgehammer_tactics.ML" -declare [[proofs = 0]] +ML {* Proofterm.proofs := 0 *} declare [[show_consts]] (* for Refute *) declare [[smt_oracle]]