equal
deleted
inserted
replaced
29 that must be punished by instant rejection. |
29 that must be punished by instant rejection. |
30 |
30 |
31 |
31 |
32 This document shows you how to make Isabelle and \LaTeX\ cooperate to |
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 |
33 produce ordinary looking mathematics that hides the fact that it was |
34 typeset by a machine. You merely need to import theory |
34 typeset by a machine. You merely need to load the right files: |
35 \texttt{LaTeXsugar} in the header of your own theory and copy the bits |
35 \begin{itemize} |
36 of \texttt{OptionalSugar} that you want to use. You may also need |
36 \item Import theory \texttt{LaTeXsugar} in the header of your own |
37 additional \LaTeX\ packages. These should be included at the beginning |
37 theory. You may also want bits of \texttt{OptionalSugar}, which you can |
38 of your \LaTeX\ document, typically in \texttt{root.tex}. |
38 copy selectively into your own theory or import as a whole. Both |
39 |
39 theories live in \texttt{HOL/Library} and are found automatically. |
40 The theories and support files are available from \cite{tar}. |
40 |
|
41 \item Should you need additional \LaTeX\ packages (the text will tell |
|
42 you so), you include them at the beginning of your \LaTeX\ document, |
|
43 typically in \texttt{root.tex}. |
|
44 \end{itemize} |
41 *} |
45 *} |
42 |
46 |
43 section{* HOL syntax*} |
47 section{* HOL syntax*} |
44 |
48 |
45 subsection{* Logic *} |
49 subsection{* Logic *} |
137 \begin{center} |
141 \begin{center} |
138 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
142 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
139 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
143 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
140 \end{center} |
144 \end{center} |
141 |
145 |
142 Limitations: premises and conclusion must each not be longer than the line. |
146 Limitations: 1. Premises and conclusion must each not be longer than |
|
147 the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again |
|
148 displayed with a horizontal line, which looks at least unusual. |
|
149 |
143 *} |
150 *} |
144 |
151 |
145 subsection{*If-then*} |
152 subsection{*If-then*} |
146 |
153 |
147 text{* If you prefer a fake ``natural language'' style you can produce |
154 text{* If you prefer a fake ``natural language'' style you can produce |
148 the body of |
155 the body of |
149 \newtheorem{theorem}{Theorem} |
156 \newtheorem{theorem}{Theorem} |
150 \begin{theorem} |
157 \begin{theorem} |
151 @{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]} |
158 @{thm[mode=IfThen] zle_trans[no_vars]} |
152 \end{theorem} |
159 \end{theorem} |
153 by typing |
160 by typing |
154 \begin{quote} |
161 \begin{quote} |
155 \verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}! |
162 \verb!@!\verb!{thm[mode=IfThen] le_trans[no_vars]}! |
156 \end{quote} |
163 \end{quote} |
157 |
164 |
158 In order to prevent odd line breaks, the premises are put into boxes. |
165 In order to prevent odd line breaks, the premises are put into boxes. |
159 At times this is too drastic: |
166 At times this is too drastic: |
160 \begin{theorem} |
167 \begin{theorem} |