Lines Matching defs:terms
16 \item A tool for embedding pretty-printed HOL theorems, terms and
958 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.
1062 (The important characteristics of the \texttt{alltt} environment are that it respects layout in terms of newlines, while also allowing the insertion of \LaTeX{} commands.
1081 Causes the string to be parsed in such a way that any embedded \texttt{case} terms are only partly parsed, allowing their input form to appear when they are output.
1142 In this way, large complicated terms that are not themselves theorems (or even of boolean type), can be stored in \HOL{} theories, and then printed in \LaTeX{} documents.
1413 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.
1507 Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands.
1508 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.
1559 These commands cite multiple theorems, terms or types.
1562 \texttt{\bs{}citePureHOLty\{id\}}] These commands\linebreak cite a theorems, terms or types.
1569 theorems, terms or types, but not typeset anything. These commands
1575 of all theorems, terms and types cited in the document. There are
1581 Theorems use by default short entries, while terms and types use
1590 \paragraph{Defining and formatting terms, types and theorems}
1726 (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.)