Lines Matching refs:function
136 $\obj{CHOOSE}\,n\,k$, where $\obj{CHOOSE}$ is a function defined by
192 says that any base case and inductive case identifies a unique function,
202 Given the theorem \verb@prim_rec@, the builtin function
203 \verb@prove_rec_fn_exists@ can prove that there is a function that satisfies
218 easy to prove there is a function which satisfies the original three
359 which can be coded as the \ML{} function \verb@SPEC_EQ@:
471 Hilbert's $\epsilon$-operator to specify a function \verb@Id@ such that
474 is unique. The first step is to prove that there exists a function \verb@Id@
554 a function \verb@Inv@ so that, if \verb@Group plus@ holds, then the
555 element \verb@Inv plus a@ is an inverse of \verb@a@. The function
558 function \verb@Inv@ with the property desired:
763 The constant \verb@RANGE@, which is a curried function of two numbers,
844 Note that an indexed term $a_i$ is represented in \HOL{} as a function
869 curried function as follows: