--- a/src/HOL/Tools/atp-inputs/full_combIK.tptp Sun Oct 01 03:07:12 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%ID: $Id$
-%Author: Jia Meng, NICTA
-%full-typed combinator reduction for I, K
-
-%K P Q --> P
-input_clause(a1,axiom,
-[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBK,tc_fun(A,tc_fun(B,A))),typeinfo(P,A)),tc_fun(B,A)),typeinfo(Q,B)),A),typeinfo(P,A))]).
-
-%I P --> P
-input_clause(a3,axiom,
-[++equal(typeinfo(hAPP(typeinfo(c_COMBI,tc_fun(T,T)),typeinfo(P,T)),T),typeinfo(P,T))]).