NEWS
changeset 17117 e2bed9e82454
parent 17097 78f1b66f70a4
child 17139 165c97f9bb63
equal deleted inserted replaced
17116:dda6c353b4ce 17117:e2bed9e82454
    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