Lines Matching refs:function
22 is an \ML\ function of type \ml{conv} (\ie\ a conversion) that
149 this exception appropriately. The standard function \ml{QCONV} is
319 subterm of a term, the function \ml{DEPTH\_CONV} can be applied to $c$:
363 \noindent The function \ml{TOP\_DEPTH\_CONV}
386 Finally, the simpler function \ml{ONCE\_DEPTH\_CONV} is provided:
507 The function \ml{FIRST\_CONV}
545 The function \ml{EVERY\_CONV} applies a list of conversions in sequence.
625 \noindent The function \ml{SUB\_CONV}
821 and the successor function \ml{SUC}, then:
916 done component-wise, and function applications are effectively
944 Skolemization (using existentially quantified function variables
980 as the name of the skolem function it introduces. For example:
1151 \noindent as shown below. The function \ml{"PRE"} is the usual
1152 predecessor function.