diff -r fe43977e434f -r d27bb852c430 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Thu Apr 26 21:58:16 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 12:16:10 2012 +0200 @@ -15,4 +15,8 @@ declare [[show_consts]] (* for Refute *) declare [[smt_oracle]] +(* +ML {* ATP_Problem_Import.isabelle_tptp_file 100 "$TPTP/Problems/PUZ/PUZ107^5.p" *} +*) + end