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