doc-src/Ref/syntax.tex
changeset 9695 ec7d7f877712
parent 9350 d855d9d1add9
child 14893 55e83c32cdec
     1.1 --- a/doc-src/Ref/syntax.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Ref/syntax.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -688,11 +688,11 @@
     1.4  \section{Translation functions} \label{sec:tr_funs}
     1.5  \index{translations|(}
     1.6  %
     1.7 -This section describes the translation function mechanism.  By writing
     1.8 -\ML{} functions, you can do almost everything to terms or \AST{}s
     1.9 -during parsing and printing.  The logic \LK\ is a good example of
    1.10 -sophisticated transformations between internal and external
    1.11 -representations of sequents; here, macros would be useless.
    1.12 +This section describes the translation function mechanism.  By writing \ML{}
    1.13 +functions, you can do almost everything to terms or \AST{}s during parsing and
    1.14 +printing.  The logic LK is a good example of sophisticated transformations
    1.15 +between internal and external representations of sequents; here, macros would
    1.16 +be useless.
    1.17  
    1.18  A full understanding of translations requires some familiarity
    1.19  with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},