Lines Matching defs:types
17 types in \LaTeX{} documents.
405 A make-file consists of two types of entries, variable definitions and
947 When writing documents in \LaTeX{} about one's favourite \HOL{} development, one frequently wants to include pretty-printed terms, types and theorems from that development.
1214 Causes the term or theorem to be printed with the \texttt{types} trace set to level~$n$.
1317 If $\mathit{nm}_1$ and $\mathit{nm}_2$ both begin with the colon character then they are parsed as types, and type instantiation is performed on the term or theorem argument instead of variable substitution.
1387 The theories specified as arguments to \mkmunge{} determine what theorems are in scope for calls to \holthm, and also determine the grammars that will govern the parsing and printing of the \HOL{} types, terms and theorems.
1481 Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands.
1482 This allows it to generate an index of all \HOL{}-theorems, types and terms that occur in the document as well as providing citation commands for \HOL{} entities in this index.
1533 These commands cite multiple theorems, terms or types.
1536 \texttt{\bs{}citePureHOLty\{id\}}] These commands\linebreak cite a theorems, terms or types.
1543 theorems, terms or types, but not typeset anything. These commands
1549 of all theorems, terms and types cited in the document. There are
1550 two types of entries in the index: long and short ones. Short
1555 Theorems use by default short entries, while terms and types use
1564 \paragraph{Defining and formatting terms, types and theorems}
1584 There are the following entry types
1701 (Of course, \emph{tokens} aren't defined \textit{per se}, but the definition of particular constants will naturally give rise to the generation of corresponding tokens when those constants appear in HOL terms, types or theorems.)