equal
deleted
inserted
replaced
219 \end{itemize} |
219 \end{itemize} |
220 For example, ``from @{thm_style prem2 conjI} and |
220 For example, ``from @{thm_style prem2 conjI} and |
221 @{thm_style prem1 conjI} we conclude @{thm_style concl conjI}'' |
221 @{thm_style prem1 conjI} we conclude @{thm_style concl conjI}'' |
222 is produced by |
222 is produced by |
223 \begin{quote} |
223 \begin{quote} |
224 \verb!from !\verb!@!\verb!{thm_style prem2 conjI}!\\ |
224 \verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\ |
225 \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\ |
|
226 \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}! |
225 \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}! |
227 \end{quote} |
226 \end{quote} |
228 Thus you can rearrange or hide premises and typeset the theorem as you like. |
227 Thus you can rearrange or hide premises and typeset the theorem as you like. |
229 The \verb!thm_style! antiquotation is a general mechanism explained |
228 The \verb!thm_style! antiquotation is a general mechanism explained |
230 in \S\ref{sec:styles}. |
229 in \S\ref{sec:styles}. |