ALL is a flag setting or other piece of information.
A flag setting for REWRITE-EQUALITIES.
When rewriting an equality (during a ND proof or when constructing
an etree), rewrite every equality as follows:
to an equivalence for those of type OOO,
to the extensional form
[lambda f(AB) lambda g(AB) forall x(B) f x = g x]
for those of type O(AB)(AB)
to the Leibniz form
[lambda x(A) lambda y(A) forall q(OA). q x implies q y]
for those of type OAA.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage