Lines Matching refs:function
4 for the HOL system~\cite{description}. The main function is a partial decision
10 The main function, \ml{ARITH\_CONV}, is a partial decision procedure for
18 contain variables are not included in the subset, but the function
33 The function makes use of a number of preprocessors\index{preprocessors} which
36 the predecessor function {\small\verb%PRE%}, and conditional
37 statements\index{conditional statements} can be eliminated using the function
40 of universally quantified formulae to be accepted. There is also a function
47 The main function, \ml{ARITH\_CONV}, is constructed from two separate
78 function \ml{load\_library}\index{load\_library@{\ptt load\_library}} (see the
124 It is easy to define a function which returns a theorem directly corresponding
155 function that proves formulae either true or false, but this would be
159 \ml{NEGATE\_CONV ARITH\_CONV} as appropriate. A combined function is