93 document practical applications. The ML antiquotation prints |
93 document practical applications. The ML antiquotation prints |
94 type-checked ML expressions verbatim. |
94 type-checked ML expressions verbatim. |
95 |
95 |
96 * Markup commands 'chapter', 'section', 'subsection', 'subsubsection', |
96 * Markup commands 'chapter', 'section', 'subsection', 'subsubsection', |
97 and 'text' support optional locale specification '(in loc)', which |
97 and 'text' support optional locale specification '(in loc)', which |
98 specifies the default context for interpreting antiquotations. |
98 specifies the default context for interpreting antiquotations. For |
99 For example: 'text (in LC) {* @{thm fold_cummute}*}'. |
99 example: 'text (in lattice) {* @{thm inf_assoc}*}'. |
100 |
100 |
101 * Option 'locale=NAME' of antiquotations specifies an alternative |
101 * Option 'locale=NAME' of antiquotations specifies an alternative |
102 context interpreting the subsequent argument. For example: @{thm |
102 context interpreting the subsequent argument. For example: @{thm |
103 [locale=LC] fold_commute}. |
103 [locale=lattice] inf_assoc}. |
104 |
104 |
105 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within |
105 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within |
106 a proof context. |
106 a proof context. |
107 |
107 |
108 * Proper output of antiquotations for theory commands involving a |
108 * Proper output of antiquotations for theory commands involving a |