NEWS
changeset 17393 23b7e14ce640
parent 17389 b4743198b939
child 17397 4ef3da248c48
equal deleted inserted replaced
17392:a639d580b34b 17393:23b7e14ce640
    90 
    90 
    91   @{ML text}
    91   @{ML text}
    92 
    92 
    93 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
    93 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
    94 definitions, equations, inequations etc., 'concl' printing only the
    94 definitions, equations, inequations etc., 'concl' printing only the
    95 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem9'
    95 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19'
    96 to print the specified premise.  TermStyle.add_style provides an ML
    96 to print the specified premise.  TermStyle.add_style provides an ML
    97 interface for introducing further styles.  See also the "LaTeX Sugar"
    97 interface for introducing further styles.  See also the "LaTeX Sugar"
    98 document practical applications.  The ML antiquotation prints
    98 document practical applications.  The ML antiquotation prints
    99 type-checked ML expressions verbatim.
    99 type-checked ML expressions verbatim.
   100 
   100