doc-src/Ref/syntax.tex

--- a/doc-src/Ref/syntax.tex	Wed Jul 02 11:59:10 1997 +0200
+++ b/doc-src/Ref/syntax.tex	Wed Jul 02 16:46:36 1997 +0200
@@ -114,7 +114,7 @@
 \begin{itemize}
 \item Name tokens: $\astofpt{t} = \Variable s$, where $t$ is an \ndx{id},
   \ndx{var}, \ndx{tid}, \ndx{tvar}, \ndx{xnum} or \ndx{xstr} token, and $s$
-  its associated string. Note that for {\tt xstr} this does not include the
+  its associated string.  Note that for {\tt xstr} this does not include the
   quotes.
 
 \item Copy productions:\index{productions!copy}
@@ -606,7 +606,7 @@
 The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
 declaration.  Hence {\tt is} is not a logical type and may be used safely as
 a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
-re-used for other enumerations of type~{\tt i} like lists or tuples. If we
+re-used for other enumerations of type~{\tt i} like lists or tuples.  If we
 had needed polymorphic enumerations, we could have used the predefined
 nonterminal symbol \ndx{args} and skipped this part altogether.
 
@@ -850,7 +850,7 @@
 constraint might appear.
 
 Also note that we are responsible to mark free identifiers that
-actually represent bound variables. This is achieved by
+actually represent bound variables.  This is achieved by
 \ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above.
 Failing to do so may cause these names to be printed in the wrong
 style.  \index{translations|)} \index{syntax!transformations|)}
@@ -861,24 +861,24 @@
 %
 Isabelle's meta-logic features quite a lot of different kinds of
 identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free},
-{\em bound}, {\em var}. One might want to have these printed in
+{\em bound}, {\em var}.  One might want to have these printed in
 different styles, e.g.\ in bold or italic, or even transcribed into
 something more readable like $\alpha, \alpha', \beta$ instead of {\tt
-  'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations
+  'a}, {\tt 'aa}, {\tt 'b} for type variables.  Token translations
 provide a means to such ends, enabling the user to install certain
 \ML{} functions associated with any logical \rmindex{token class} and
 depending on some \rmindex{print mode}.
 
 The logical class of identifiers can not necessarily be determined by
-its syntactic category, though. For example, consider free vs.\ bound
-variables. So Isabelle's pretty printing mechanism, starting from
+its syntactic category, though.  For example, consider free vs.\ bound
+variables.  So Isabelle's pretty printing mechanism, starting from
 fully typed terms, has to be careful to preserve this additional
 information\footnote{This is done by marking atoms in abstract syntax
-  trees appropriately. The marks are actually visible by print
+  trees appropriately.  The marks are actually visible by print
   translation functions -- they are just special constants applied to
   atomic asts, for example \texttt{("_bound" x)}.}.  In particular,
 user-supplied print translation functions operating on terms have to
-be well-behaved in this respect. Free identifiers introduced to
+be well-behaved in this respect.  Free identifiers introduced to
 represent bound variables have to be marked appropriately (cf.\ the
 example at the end of \S\ref{sec:tr_funs}).
 
@@ -890,12 +890,12 @@
 \end{ttbox}\index{token_translation}
 The elements of this list are of the form $(m, c, f)$, where $m$ is a
 print mode identifier, $c$ a token class, and $f\colon string \to
-string \times int$ the actual translation function. Assuming that $x$
+string \times int$ the actual translation function.  Assuming that $x$
 is of identifier class $c$, and print mode $m$ is the first one of all
 currently active modes that provide some translation for $c$, then $x$
-is output according to $f(x) = (x', len)$. Thereby $x'$ is the
+is output according to $f(x) = (x', len)$.  Thereby $x'$ is the
 modified identifier name and $len$ its visual length approximated in
-terms of whole characters. Thus $x'$ may include non-printing parts
+terms of whole characters.  Thus $x'$ may include non-printing parts
 like control sequences or markup information for typesetting systems.
 
 %FIXME example (?)