changeset 20647 | 680b58597f65 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/atp-inputs/const_combIK.tptp Wed Sep 20 14:02:41 2006 +0200 @@ -0,0 +1,12 @@ +%ID: $Id$ +%Author: Jia Meng, NICTA +%const-typed combinator reduction for I, K + +%K P Q --> P +input_clause(a1,axiom, +[++equal(hAPP(hAPP(c_COMBK(A,B),P),Q),P)]). + +%I P --> P +input_clause(a3,axiom, +[++equal(hAPP(c_COMBI(T),P),P)]). +