doc-src/Ref/syntax.tex

              | Appl of ast list
 \end{ttbox}
 %
 Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
 atoms are shown as quoted strings, variable atoms as non-quoted strings and
-applications as a parenthesized list of subtrees.  For example, the \AST
+applications as a parenthesised list of subtrees.  For example, the \AST
 \begin{ttbox}
 Appl [Constant "_constrain",
       Appl [Constant "_abs", Variable "x", Variable "t"],
       Appl [Constant "fun", Variable "'a", Variable "'b"]]
 \end{ttbox}

     \[ \astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = 
        \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}}
     \]
 \end{itemize}
 %
-Type constraints are inserted to allow the printing of types.  This is
-governed by the boolean variable \ttindex{show_types}:
+Type constraints\index{type constraints} are inserted to allow the printing
+of types.  This is governed by the boolean variable \ttindex{show_types}:
 \begin{itemize}
   \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
-    \ttindex{show_types} not set to {\tt true}.
+    \ttindex{show_types} is set to {\tt false}.
 
   \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, 
          \astofterm{\tau}}$ \ otherwise.  
 
     Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type

     of their sort.
 \end{itemize}
 %
 The \AST{}, after application of macros (see \S\ref{sec:macros}), is
 transformed into the final output string.  The built-in {\bf print AST
-  translations}\indexbold{translations!print AST} effectively reverse the
+  translations}\indexbold{translations!print AST} reverse the
 parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
 
 For the actual printing process, the names attached to productions
 of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
 a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or

 express all but the most obscure translations.
 
 Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
 theory.\footnote{This and the following theories are complete working
   examples, though they specify only syntax, no axioms.  The file {\tt
-    ZF/zf.thy} presents the full set theory definition, including many
+    ZF/ZF.thy} presents the full set theory definition, including many
   macro rules.}  Theory {\tt SET} defines constants for set comprehension
 ({\tt Collect}), replacement ({\tt Replace}) and bounded universal
 quantification ({\tt Ball}).  Each of these binds some variables.  Without
-additional syntax we should have to express $\forall x \in A.  P$ as {\tt
+additional syntax we should have to write $\forall x \in A.  P$ as {\tt
   Ball(A,\%x.P)}, and similarly for the others.
 
 \begin{figure}
 \begin{ttbox}
 SET = Pure +

 
 \begin{warn}
 If \ttindex{eta_contract} is set to {\tt true}, terms will be
 $\eta$-contracted {\em before\/} the \AST{} rewriter sees them.  Thus some
 abstraction nodes needed for print rules to match may vanish.  For example,
-\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does
+\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does
 not apply and the output will be {\tt Ball(A, P)}.  This problem would not
 occur if \ML{} translation functions were used instead of macros (as is
 done for binder declarations).
 \end{warn}
 

 
 
 \subsection{Applying rules}
 As a term is being parsed or printed, an \AST{} is generated as an
 intermediate form (recall Fig.\ts\ref{fig:parse_print}).  The \AST{} is
-normalized by applying macro rules in the manner of a traditional term
+normalised by applying macro rules in the manner of a traditional term
 rewriting system.  We first examine how a single rule is applied.
 
-Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some
+Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some
 translation rule.  A subtree~$u$ of $t$ is a {\bf redex} if it is an
 instance of~$l$; in this case $l$ is said to {\bf match}~$u$.  A redex
 matched by $l$ may be replaced by the corresponding instance of~$r$, thus
 {\bf rewriting} the \AST~$t$.  Matching requires some notion of {\bf
   place-holders} that may occur in rule patterns but not in ordinary

 translations
   "[]"    == "Nil"
 \end{ttbox}
 The term {\tt Nil} will be printed as {\tt []}, just as expected.
 The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
-expected! 
+expected!  How is the type~{\tt Nil} printed?
 
 Normalizing an \AST{} involves repeatedly applying macro rules until none
-is applicable.  Macro rules are chosen in the order that they appear in the
+are applicable.  Macro rules are chosen in the order that they appear in the
 {\tt translations} section.  You can watch the normalization of \AST{}s
 during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
 {\tt true}.\index{tracing!of macros} Alternatively, use
 \ttindex{Syntax.test_read}.  The information displayed when tracing
 includes the \AST{} before normalization ({\tt pre}), redexes with results

 two elements, binding the first to {\tt x} and the rest to {\tt xs}.
 Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.  
 The parse rules only work in the order given.
 
 \begin{warn}
-  The \AST{} rewriter cannot discern constants from variables and looks
+  The \AST{} rewriter cannot distinguish constants from variables and looks
   only for names of atoms.  Thus the names of {\tt Constant}s occurring in
   the (internal) left-hand side of translation rules should be regarded as
   \rmindex{reserved words}.  Choose non-identifiers like {\tt\at Finset} or
   sufficiently long and strange names.  If a bound variable's name gets
   rewritten, the result will be incorrect; for example, the term
 \begin{ttbox}
 \%empty insert. insert(x, empty)
 \end{ttbox}
-  gets printed as \verb|%empty insert. {x}|.
+\par\noindent is printed as \verb|%empty insert. {x}|.
 \end{warn}
 
 
 \subsection{Example: a parse macro for dependent types}\label{prod_trans}
 \index{examples!of macros}

 \index{translations|(} 
 %
 This section describes the translation function mechanism.  By writing
 \ML{} functions, you can do almost everything with terms or \AST{}s during
 parsing and printing.  The logic \LK\ is a good example of sophisticated
-transformations between internal and external representations of
-associative sequences; here, macros would be useless.
+transformations between internal and external representations of sequents;
+here, macros would be useless. 
 
 A full understanding of translations requires some familiarity
 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
 {\tt Syntax.ast} and the encodings of types and terms as such at the various
 stages of the parsing or printing process.  Most users should never need to

         in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts)
         end
       else list_comb (Const (r, dummyT) $ A $ B, ts)
   | dependent_tr' _ _ = raise Match;
 \end{ttbox}
-The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried
-function application during its installation.  We could set up print
-translations for both {\tt Pi} and {\tt Sigma} by including
+The argument {\tt (q,r)} is supplied to the curried function {\tt
+  dependent_tr'} by a partial application during its installation.  We
+can set up print translations for both {\tt Pi} and {\tt Sigma} by
+including
 \begin{ttbox}\index{*ML section}
 val print_translation =
   [("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
    ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))];
 \end{ttbox}
 within the {\tt ML} section.  The first of these transforms ${\tt Pi}(A,
 \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
-$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend
+$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not depend
 on~$x$.  It checks this using \ttindex{loose_bnos}, yet another function
 from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$ renamed away
-from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes
-referring to our {\tt Abs} node replaced by $\ttfct{Free} (x',
+from all names in $B$, and $B'$ is the body $B$ with {\tt Bound} nodes
+referring to the {\tt Abs} node replaced by $\ttfct{Free} (x',
 \mtt{dummyT})$.
 
 We must be careful with types here.  While types of {\tt Const}s are
 ignored, type constraints may be printed for some {\tt Free}s and
 {\tt Var}s if \ttindex{show_types} is set to {\tt true}.  Variables of type