equal
deleted
inserted
replaced
1 |
1 |
2 theory Antiquotes |
2 theory Antiquotes |
3 imports "../Base" |
3 imports "../Base" |
4 begin |
4 begin |
|
5 |
|
6 |
5 |
7 |
6 |
8 |
7 section {* Useful Document Antiquotations *} |
9 section {* Useful Document Antiquotations *} |
8 |
10 |
9 text {* |
11 text {* |
12 |
14 |
13 {\bf Solution:} This can be achieved using document antiquotations.\smallskip |
15 {\bf Solution:} This can be achieved using document antiquotations.\smallskip |
14 |
16 |
15 Document antiquotations can be used for ensuring consistent type-setting of |
17 Document antiquotations can be used for ensuring consistent type-setting of |
16 various entities in a document. They can also be used for sophisticated |
18 various entities in a document. They can also be used for sophisticated |
17 \LaTeX-hacking. |
19 \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you |
|
20 obtain a list of all available document antiquotations and their options. |
18 |
21 |
19 Below we give the code for two antiquotations that can be used to typeset |
22 Below we give the code for two additional antiquotations that can be used to typeset |
20 ML-code and also to check whether the given code actually compiles. This |
23 ML-code and also to check whether the given code actually compiles. This |
21 provides a sanity check for the code and also allows one to keep documents |
24 provides a sanity check for the code and also allows one to keep documents |
22 in sync with other code, for example Isabelle. |
25 in sync with other code, for example Isabelle. |
23 |
26 |
24 We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This |
27 We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This |