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 metalogical statement theorem, and 'prem1' .. 'prem9' 
90 conclusion of a metalogical 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 typechecked 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 