81 argument is a known logical constant; |
81 argument is a known logical constant; |
82 |
82 |
83 @{term_style style term} and @{thm_style style thm} print a term or |
83 @{term_style style term} and @{thm_style style thm} print a term or |
84 theorem applying a "style" to it |
84 theorem applying a "style" to it |
85 |
85 |
|
86 @{ML text} |
|
87 |
86 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of |
88 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of |
87 definitions, equations, inequations etc., 'concl' printing only the |
89 definitions, equations, inequations etc., 'concl' printing only the |
88 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9' |
90 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9' |
89 to print the specified premise. TermStyle.add_style provides an ML |
91 to print the specified premise. TermStyle.add_style provides an ML |
90 interface for introducing further styles. See also the "LaTeX Sugar" |
92 interface for introducing further styles. See also the "LaTeX Sugar" |
91 document practical applications. |
93 document practical applications. The ML antiquotation prints |
|
94 type-checked ML expressions verbatim. |
92 |
95 |
93 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within |
96 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within |
94 a proof context. |
97 a proof context. |
95 |
98 |
96 * Proper output of antiquotations for theory commands involving a |
99 * Proper output of antiquotations for theory commands involving a |