7 \section{Introduction} |
7 \section{Introduction} |
8 |
8 |
9 This document is for those Isabelle users who have mastered |
9 This document is for those Isabelle users who have mastered |
10 the art of mixing \LaTeX\ text and Isabelle theories and never want to |
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 |
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]}! |
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,eta_contract=false] setsum_cartesian_product[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}, |
70 \begin{itemize} |
70 \begin{itemize} |
71 \item @{term"{x. P}"} instead of @{text"{x. P}"}. |
71 \item @{term"{x. P}"} instead of @{text"{x. P}"}. |
72 \item @{term"{}"} instead of @{text"{}"}, where |
72 \item @{term"{}"} instead of @{text"{}"}, where |
73 @{term"{}"} is also input syntax. |
73 @{term"{}"} is also input syntax. |
74 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
74 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
|
75 \item @{term"card A"} instead of @{text"card A"}. |
75 \end{itemize} |
76 \end{itemize} |
76 |
77 |
77 |
78 |
78 \subsection{Lists} |
79 \subsection{Lists} |
79 |
80 |
80 If lists are used heavily, the following notations increase readability: |
81 If lists are used heavily, the following notations increase readability: |
81 \begin{itemize} |
82 \begin{itemize} |
82 \item @{term"x # xs"} instead of @{text"x # xs"}, |
83 \item @{term"x # xs"} instead of @{text"x # xs"}, |
83 where @{term"x # xs"} is also input syntax. |
84 where @{term"x # xs"} is also input syntax. |
84 If you prefer more space around the $\cdot$ you have to redefine |
|
85 \verb!\isasymcdot! in \LaTeX: |
|
86 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
|
87 |
|
88 \item @{term"length xs"} instead of @{text"length xs"}. |
85 \item @{term"length xs"} instead of @{text"length xs"}. |
89 \item @{term"nth xs n"} instead of @{text"nth xs n"}, |
86 \item @{term"nth xs n"} instead of @{text"nth xs n"}, |
90 the $n$th element of @{text xs}. |
87 the $n$th element of @{text xs}. |
91 |
88 |
92 \item Human readers are good at converting automatically from lists to |
89 \item Human readers are good at converting automatically from lists to |