Lines Matching refs:function
17 describing concrete types used by the function \ml{define\_type}, the type
27 function \ml{ASCII} to the eight boolean values of its standard ascii character
36 in logic by a value of type \ml{ascii} constructed using the function constant
40 library using the function \ml{define\_type} from the \HOL\ recursive types
57 \index{function definitions!on type {\tt ascii}|(}
62 loaded into \HOL, one can use this rule of definition to define a function that
74 \noindent In fact, any function whatsoever on the \ml{ascii} is definable
77 \index{function definitions!on type {\tt ascii}|)}
88 the function \ml{ASCII} is injective:
124 using the function \ml{ASCII} and can be used, for example, with
174 ascii character codes. These sequences are constructed using the function
199 \index{function definitions!on type {\tt string}|(}
217 \index{function definitions!on type {\tt string}|)}
399 function \ml{load\_library} (see the \HOL\ manual for a general description of
476 \subsection{The {\tt load\_string} function}%
493 sequence defines an \ML\ function called \ml{load\_string} in the current \HOL\
496 function can then be used to complete loading of the library. Evaluating
503 into \HOL\ and activates autoloading from its theory files. The function
507 Note that the function \ml{load\_string} becomes available when loading the