12 bliss of writing \verb!@!\verb!{thm[display,mode=latex_sum] setsum_Suc_diff [no_vars]}! |
12 bliss of writing \verb!@!\verb!{thm[display,mode=latex_sum] setsum_Suc_diff [no_vars]}! |
13 and seeing Isabelle typeset it for them: |
13 and seeing Isabelle typeset it for them: |
14 @{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]} |
14 @{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]} |
15 No typos, no omissions, no sweat. |
15 No typos, no omissions, no sweat. |
16 If you have not experienced that joy, read Chapter 4, \emph{Presenting |
16 If you have not experienced that joy, read Chapter 4, \emph{Presenting |
17 Theories}, \cite{LNCS2283} first. |
17 Theories}, @{cite LNCS2283} first. |
18 |
18 |
19 If you have mastered the art of Isabelle's \emph{antiquotations}, |
19 If you have mastered the art of Isabelle's \emph{antiquotations}, |
20 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity |
20 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity |
21 you may be tempted to think that all readers of the stunning ps or pdf |
21 you may be tempted to think that all readers of the stunning ps or pdf |
22 documents you can now produce at the drop of a hat will be struck with |
22 documents you can now produce at the drop of a hat will be struck with |
178 |
178 |
179 |
179 |
180 \subsection{Inference rules} |
180 \subsection{Inference rules} |
181 |
181 |
182 To print theorems as inference rules you need to include Didier |
182 To print theorems as inference rules you need to include Didier |
183 R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
183 R\'emy's \texttt{mathpartir} package~@{cite mathpartir} |
184 for typesetting inference rules in your \LaTeX\ file. |
184 for typesetting inference rules in your \LaTeX\ file. |
185 |
185 |
186 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
186 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
187 @{thm[mode=Rule] conjI}, even in the middle of a sentence. |
187 @{thm[mode=Rule] conjI}, even in the middle of a sentence. |
188 If you prefer your inference rule on a separate line, maybe with a name, |
188 If you prefer your inference rule on a separate line, maybe with a name, |