Lines Matching defs:For
107 this document. For similar reasons, also explained later, much of the
169 this command. For A4 size paper, the appropriate command is `{\tt \bk
170 Afourtrue}' (the distribution default). For American paper, the command should
270 individual steps required in this process. For a full description of the {\tt
533 The format of \doc\ files for theorems is simple. For each theorem, there is
577 \ml{f} and \ml{g} are functions that yield values of type \ml{one}. For
582 system is built, but which are not stored in any theory file. For these
678 the names of built-in \ML\ functions. For each identifier \meta{name}, there
725 `{\small\verb!$!}'. For example, the \meta{name} field for the tactical
758 \ML\ function, it must be preceded by the dollar sign `{\small\verb!$!}'. For
799 be misleading as to the nature of the \ML\ function in question. For example,
903 followed by a single space and the name of the library. For example:
968 both failure and looping can occur. For some functions, it may be difficult to
969 give both necessary and sufficient conditions for failure. For example, the
1053 contexts in which it might be used. For example, suppose that the
1214 commentary, the `displayed' text is not indented. For example, in: