Lines Matching defs:Theory
48 \item [Theory facts.]
52 As such theorems are pretty-printed into the corresponding \texttt{Theory.sig} file, the help system will find both the declaration in the signature (\eg, \ml{val~nm~:thm}), and the entry for that theorem in the comment-block.
140 \subsection{Theory construction}
164 The file that generates the \HOL{} theory \textit{my}\texttt{Theory} must be called \textit{my}\texttt{Script.sml}.
234 Finally, take care not to have the string ``\texttt{Theory}'' appear at the end of the name of any of your files.
236 This will also remove other files with names containing ``\texttt{Theory.sml}'' or ``\texttt{Theory.sig}''.
292 As a special case of this, targets ending with the suffix \ml{Theory} are treated as an instruction to build the theory files that lie behind a \HOL{} theory.
366 However, it will still attempt to do ``\HOL{} things'' with files whose names end in \texttt{Script} and \texttt{Theory}.
1404 \mkmunge \(\langle\mathit{thy}\sb{1}\rangle\)Theory ... \(\langle\mathit{thy}\sb{n}\rangle\)Theory