src/HOL/TPTP/ATP_Problem_Import.thy
changeset 47670 24babc4b1925
parent 47557 32f35b3d9e42
child 47714 d6683fe037b1
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Apr 22 14:16:46 2012 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  uses ("atp_problem_import.ML")
     1.5  begin
     1.6  
     1.7 +declare [[show_consts]] (* for Refute *)
     1.8 +
     1.9  typedecl iota (* for TPTP *)
    1.10  
    1.11  use "atp_problem_import.ML"