Lines Matching refs:function
41 The type definition package (i.e. the \ML\ function
163 The \ml{install} function now sets the search path to:
173 The function
191 \ml{library\_pathname} can be changed by users only via the \ml{install} function.
216 displaying help files. This default can be changed with the \ML\ function:
223 \noindent This installs a new user-supplied help function, and returns the
231 into the current help function,
261 and these two function are analogous to the \ML\ functions
318 with the function:
481 the infixed function \ml{INSERT} adds an element to a set.
521 of the paired abstraction is an unspecified function of the structure
709 associated with a function on strings. When such a block is
712 associated function is applied. Syntax blocks can be used with the
717 The ML function:
727 argument is the name of a function having a type which is an instance
762 The following function is useful with syntax blocks, because it enables
786 terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag
788 whatever \ML\ function is currently bound to the name
809 The function:
852 different definition of the function
938 and the successor function \ml{SUC}, then:
1033 done component-wise, and function applications are effectively
1061 Skolemization (using existentially quantified function variables
1097 as the name of the skolem function it introduces. For example: