changeset 20647 | 680b58597f65 |
child 20660 | 8606ddd42554 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/atp-inputs/u_combS_e.tptp Wed Sep 20 14:02:41 2006 +0200 @@ -0,0 +1,7 @@ +%ID: $Id$ +%Author: Jia Meng, NICTA +%untyped combinator reduction for S' + +%S' c f g x --> c (f x) (g x) +input_clause(a8,axiom, +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).