doc-src/IsarRef/generic.tex
changeset 19363 667b5ea637dd
parent 19145 990f59414e34
child 19379 c8cf1544b5a7
     1.1 --- a/doc-src/IsarRef/generic.tex	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    'definition' locale? (constdecl? constdef +)
     1.5    ;
     1.6  
     1.7 -  'abbreviation' locale? '(output)'? (constdecl? prop +)
     1.8 +  'abbreviation' locale? mode? (constdecl? prop +)
     1.9    ;
    1.10    'axiomatization' locale? consts? ('where' specs)?
    1.11    ;
    1.12 @@ -55,16 +55,20 @@
    1.13    supported here.
    1.14    
    1.15  \item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
    1.16 -  a syntactic constant which is associated with a certain term derived
    1.17 -  from the specification given as $eq$.  The very same transformations
    1.18 -  as for $\isarkeyword{definition}$ are applied here, although
    1.19 -  additional conditions are not supported.
    1.20 +  a syntactic constant which is associated with a certain term
    1.21 +  according to the meta-level equality $eq$.
    1.22    
    1.23    Abbreviations participate in the usual type-inference process, but
    1.24 -  are expanded before the logic ever sees them.  The expansion is
    1.25 -  one-way by default; the ``$(output)$'' option makes abbreviations
    1.26 -  fold back whenever terms are pretty printed.  The latter needs some
    1.27 -  care to avoid overlapping or looping syntactic replacements!
    1.28 +  are expanded before the logic ever sees them.  Pretty printing of
    1.29 +  terms involves higher-order rewriting with rules stemming from
    1.30 +  reverted abbreviations.  This needs some care to avoid overlapping
    1.31 +  or looping syntactic replacements!
    1.32 +  
    1.33 +  The optional $mode$ specification restricts output to a particular
    1.34 +  print mode; using ``$input$'' here achieves the effect of one-way
    1.35 +  abbreviations.  The mode may also include an ``$output$'' qualifier
    1.36 +  that affects the concrete syntax declared for abbreviations, cf.\ 
    1.37 +  $\isarkeyword{syntax}$ in \S\ref{sec:syn-trans}.
    1.38    
    1.39  \item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
    1.40    \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants