src/HOL/TPTP/ATP_Problem_Import.thy
changeset 47714 d6683fe037b1
parent 47670 24babc4b1925
child 47765 18f37b7aa6a6
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Tue Apr 24 09:47:40 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Tue Apr 24 09:47:40 2012 +0200
     1.3 @@ -11,8 +11,6 @@
     1.4  
     1.5  declare [[show_consts]] (* for Refute *)
     1.6  
     1.7 -typedecl iota (* for TPTP *)
     1.8 -
     1.9  use "atp_problem_import.ML"
    1.10  
    1.11  end