src/HOL/Tools/atp-inputs/const_combS.dfg

rearranged axioms and simp rules for scaleR

%ID: $Id$
%Author: Jia Meng, NICTA
%const-typed combinator reduction for S

clause(
forall([A, B, C, P, Q, R],
or( equal(hAPP(hAPP(hAPP(c_COMBS(A,B,C),P),Q),R),hAPP(hAPP(P,R),hAPP(Q,R))))),
a2 ).