Lines Matching refs:function
28 token. 4. Parsing a function symbol in some cases requires that
29 the function arguments have been parsed (e.g., to instantiate
40 functions. 4. Each parsing function maps a (possibly empty) list
41 of function arguments (parsed as HOL terms) to the HOL term that
42 results from applying the (function corresponding to the) token
44 valid. 'parse_term' uses the result of the first parsing function
45 that does not raise 'HOL_ERR'. 5. Each parsing function
54 dictionary entry for a token (or every parsing function in its
56 of the first parsing function in the entry for "_" that does not
443 declared function symbols, and a list of asserted formulas *)