Lines Matching defs:terms
14 terms, signatures, theorems and theories, tactics and tacticals.
22 This section describes the concrete syntax for types, terms and theorems,
71 \subsection{Syntax of types and terms}
72 \index{classes!built-in|bold}\index{syntax!of types and terms}
99 \index{terms!syntax of|bold}\index{type constraints}
119 are just terms of type~\texttt{prop}.
189 resulting theorem. Scheme variables in a goal may be replaced by terms
342 none on the left in a common instance of these terms. Choosing a new
612 rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function
707 Multiple quantifiers create complex terms. Proving
800 Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt