Lines Matching defs:example
8 alternative syntaxes, for example using mathematical symbols from a
52 prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand
65 for example, {\tt?hello} has identifier {\tt"hello"} and subscript
81 classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace
193 For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as
241 Let us try an example given in~\S\ref{joining}. We
353 following example uses \ttindex{read_instantiate} to create an instance
466 \subsection{A trivial example in propositional logic}
470 first-order logic. Let us try the example from \S\ref{prop-proof},
573 assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we
933 so let us proceed to the next example: