9 text{* This document is for those Isabelle users that have mastered
10 the art of mixing \LaTeX\ text and Isabelle theories and never want to
11 typeset a theorem by hand anymore because they have experienced the
12 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
13 and seeing Isabelle typeset it for them:
14 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
15 No typos, no omissions, no sweat!
16 If you have not experienced that joy, read chapter 4, \emph{Presenting
17 Theories}, of \cite{LNCS2283} first.
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
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
23 awe at the beauty unfolding in front of their eyes. Until one day you
24 come across that very critical of readers known as the ``common referee''.
25 He has the nasty habit of refusing to understand unfamiliar notation
26 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
27 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
28 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin
29 that must be punished by immediate rejection.
32 This document shows you how to make Isabelle and \LaTeX\ cooperate to
33 produce ordinary looking mathematics that hides the fact that it was
34 typeset by a machine. This involves additional syntax-related
35 declarations for your theory file and corresponding \LaTeX\ macros. We
36 explain how to use them but show neither. They can be downloaded from
41 section "Printing theorems"
43 subsection "Inference rules"
47 "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
48 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
50 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
51 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
53 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
56 "_asm" :: "prop \<Rightarrow> asms" ("_")
59 text{* To print theorems as inference rules you need to include the
60 \texttt{Rule} output syntax declarations in your theory and Didier
61 Remy's \texttt{mathpartir} package for typesetting inference rules in
64 Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
65 @{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
66 The standard \texttt{display} attribute, i.e.\ writing
67 \verb![mode=Rule,display]! instead of \verb![mode=Rule]!,
68 displays the rule on a separate line using a smaller font:
69 @{thm[mode=Rule,display] conjI[no_vars]}
70 Centering a display does not work directly. Instead you can enclose the
71 non-displayed variant in a \texttt{center} environment:
74 \verb!\begin{center}!\\
75 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
78 also adds a label to the rule and yields
80 @{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
82 Of course you can display multiple rules in this fashion:
84 \verb!\begin{center}\isastyle!\\
85 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\
86 \verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\
87 \verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\
91 \begin{center}\isastyle
92 @{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]
93 @{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad
94 @{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$}
96 Note that we included \verb!\isastyle! to obtain
97 the smaller font that otherwise comes only with \texttt{display}.