SKOLEM-TERM is a flavor.
A skolem-term label contains both a skolem term, which is a
skolem function applied to some free variables (if any), and a parameter,
which is a new constant. Skolem-terms may be printed in either of the
two ways: the flag SHOW-SKOLEM controls how they are printed.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage