Lines Matching refs:function
96 \noindent The library \ml{taut} defines \ml{TAUT\_RULE}\footnote{The function \ml{TAUT\_RULE} has been replaced by a function called \ml{TAUT\_PROVE}
126 \ML{} function that maps a term $t_1$ to an equation:
137 Conversions are applied using the function:
144 and generates a conversion (\ie\ \ML{} function of type {\small\verb%term->thm%})
285 longer applicable to any subterms. The function \ml{TOP\_DEPTH\_CONV}
304 form. The conclusion of a theorem can be extracted with the \ML{} function
341 the infixed function:
441 system timer using the function:
505 \HOL{} already has a predefined function:
512 \HOL{} also has a predefined \ML{} function for removing repeated elements of
536 There is a predefined sorting function in \ML:
549 Using this function, the list of conjuncts of the normalization of a
550 term is easily computed. The predefined \ML{} function:
708 \noindent Given a function \ml{$f$ : thm -> tactic}, the tactic
749 popping the assumption and applying to it the function obtained by
751 function composition operator \ml{o}
809 \ml{CONJ\_EQ} is defined with the predefined function:
898 The function \ml{PROVE\_CONJ}, defined below,
946 \noindent Loading these \ML{} function definitions into \HOL:
1033 What is needed is a function that will apply a conversion to all
1034 conjunctive subterms of a term. Such a function is \ml{TOP\_DEPTH\_CONV}, however
1062 be obtained by writing a special scanning function that
1078 \noindent Next a function that conjoins the left hand sides and right
1090 \noindent Next, a function that applies a conversion $c$ to all
1091 conjunctive subterms of a term. This uses the \ML{} function:
1199 function \ml{b} backs up to the last goal.