src/HOL/Tools/atp-inputs/const_helper1.tptp

Moved the functional equality axioms to helper1 files.

%ID: $Id$
%Author: Jia Meng, NICTA
%functional equality and extensionality for const-types-only

input_clause(a9,axiom,
[--hBOOL(hAPP(hAPP(fequal(A),X),Y)),++equal(X,Y)]).

input_clause(a10,axiom,
[++hBOOL(hAPP(hAPP(fequal(A),X),Y)),--equal(X,Y)]).

input_clause(a11,axiom,
[--equal(hAPP(F,hAPP(hAPP(hEXTENT(A,B),F),G)),hAPP(G,hAPP(hAPP(hEXTENT(A,B),F),G))),
++equal(F,G)]).