equal
deleted
inserted
replaced
5 chapter {* Comments for Authors *} |
5 chapter {* Comments for Authors *} |
6 |
6 |
7 text {* |
7 text {* |
8 |
8 |
9 \begin{itemize} |
9 \begin{itemize} |
10 \item The Cookbook can be compiled on the command-line with: |
10 \item This tutorial can be compiled on the command-line with: |
11 |
11 |
12 @{text [display] "$ isabelle make"} |
12 @{text [display] "$ isabelle make"} |
13 |
13 |
14 You very likely need a recent snapshot of Isabelle in order to compile |
14 You very likely need a recent snapshot of Isabelle in order to compile |
15 the Cookbook. Some parts of the Cookbook also rely on compilation with |
15 the tutorial. Some parts of the tutorial also rely on compilation with |
16 PolyML. |
16 PolyML. |
17 |
17 |
18 \item You can include references to other Isabelle manuals using the |
18 \item You can include references to other Isabelle manuals using the |
19 reference names from those manuals. To do this the following |
19 reference names from those manuals. To do this the following |
20 four \LaTeX{} commands are defined: |
20 four \LaTeX{} commands are defined: |
29 |
29 |
30 So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
30 So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
31 in the implementation manual, namely \ichcite{ch:logic}. |
31 in the implementation manual, namely \ichcite{ch:logic}. |
32 |
32 |
33 \item There are various document antiquotations defined for the |
33 \item There are various document antiquotations defined for the |
34 Cookbook. They allow to check the written text against the current |
34 tutorial. They allow to check the written text against the current |
35 Isabelle code and also allow to show responses of the ML-compiler. |
35 Isabelle code and also allow to show responses of the ML-compiler. |
36 Therefore authors are strongly encouraged to use antiquotations wherever |
36 Therefore authors are strongly encouraged to use antiquotations wherever |
37 appropriate. |
37 appropriate. |
38 |
38 |
39 The following antiquotations are defined: |
39 The following antiquotations are defined: |
141 \end{center} |
141 \end{center} |
142 |
142 |
143 \item Functions and value bindings cannot be defined inside antiquotations; they need |
143 \item Functions and value bindings cannot be defined inside antiquotations; they need |
144 to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} |
144 to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} |
145 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
145 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
146 the Cookbook, however, ensures that the environment markers are not printed. |
146 the tutorial, however, ensures that the environment markers are not printed. |
147 |
147 |
148 \item Line numbers can be printed using |
148 \item Line numbers can be printed using |
149 \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"} |
149 \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"} |
150 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
150 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
151 |
151 |