diff -r 1e93eb09ebb9 -r f27a30a18a17 doc-src/Ref/defining.tex
--- a/doc-src/Ref/defining.tex	Wed Jul 02 11:59:10 1997 +0200
+++ b/doc-src/Ref/defining.tex	Wed Jul 02 16:46:36 1997 +0200
@@ -182,9 +182,9 @@
 \end{warn}
 
 \begin{warn}
-  Type constraints bind very weakly. For example, \verb!x<y::nat! is normally
+  Type constraints bind very weakly.  For example, \verb!x<y::nat! is normally
   parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 3 or less, in
-  which case the string is likely to be ambiguous. The correct form is
+  which case the string is likely to be ambiguous.  The correct form is
   \verb!x<(y::nat)!.
 \end{warn}
 
@@ -217,10 +217,10 @@
 Name tokens have a predefined syntax.  The lexer distinguishes six disjoint
 classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
 identifiers\index{type identifiers}, type unknowns\index{type unknowns},
-\rmindex{numerals}, \rmindex{strings}. They are denoted by \ndxbold{id},
+\rmindex{numerals}, \rmindex{strings}.  They are denoted by \ndxbold{id},
 \ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{xnum}, \ndxbold{xstr},
 respectively.  Typical examples are {\tt x}, {\tt ?x7}, {\tt 'a}, {\tt ?'a3},
-{\tt \#42}, {\tt ''foo bar''}. Here is the precise syntax:
+{\tt \#42}, {\tt ''foo bar''}.  Here is the precise syntax:
 \begin{eqnarray*}
 id        & =   & letter~quasiletter^* \\
 var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
@@ -331,7 +331,7 @@
     analysis.\index{delimiters}
 
   \item[{\tt logtypes}] lists the types that are regarded the same as {\tt
-    logic} syntactically. Thus types of object-logics (e.g.\ {\tt nat}, say)
+    logic} syntactically.  Thus types of object-logics (e.g.\ {\tt nat}, say)
     will be automatically equipped with the standard syntax of
     $\lambda$-calculus.
 
@@ -445,7 +445,7 @@
 
 \begin{warn}
   Theories must sometimes declare types for purely syntactic purposes ---
-  merely playing the role of nonterminals. One example is \tydx{type}, the
+  merely playing the role of nonterminals.  One example is \tydx{type}, the
   built-in type of types.  This is a `type of all types' in the syntactic
   sense only.  Do not declare such types under {\tt arities} as belonging to
   class {\tt logic}\index{*logic class}, for that would make them useless as
@@ -527,11 +527,11 @@
 \end{ttbox}
 
 Note that because {\tt exp} is not of class {\tt logic}, it has been
-retained as a separate nonterminal. This also entails that the syntax
+retained as a separate nonterminal.  This also entails that the syntax
 does not provide for identifiers or paranthesized expressions.
 Normally you would also want to add the declaration {\tt arities
   exp::logic} after {\tt types} and use {\tt consts} instead of {\tt
-  syntax}. Try this as an exercise and study the changes in the
+  syntax}.  Try this as an exercise and study the changes in the
 grammar.
 
 \subsection{The mixfix template}
@@ -600,7 +600,7 @@
 
 A slightly more general form of infix declarations allows constant
 names to be independent from their concrete syntax, namely \texttt{$c$
-  ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}. As
+  ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}.  As
 an example consider:
 \begin{ttbox}
 and :: [bool, bool] => bool  (infixr "&" 35)
@@ -621,7 +621,7 @@
 introduces a constant~$c$ of type~$\sigma$, which must have the form
 $(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
-and the whole term has type~$\tau@3$. The optional integer $pb$
+and the whole term has type~$\tau@3$.  The optional integer $pb$
 specifies the body's priority, by default~$p$.  Special characters
 in $\Q$ must be escaped using a single quote.
 
@@ -660,8 +660,8 @@
 \section{*Alternative print modes} \label{sec:prmodes}
 \index{print modes|(}
 %
-Isabelle's pretty printer supports alternative output syntaxes. These
-may be used independently or in cooperation. The currently active
+Isabelle's pretty printer supports alternative output syntaxes.  These
+may be used independently or in cooperation.  The currently active
 print modes (with precedence from left to right) are determined by a
 reference variable.
 \begin{ttbox}\index{*print_mode}
@@ -669,7 +669,7 @@
 \end{ttbox}
 Initially this may already contain some print mode identifiers,
 depending on how Isabelle has been invoked (e.g.\ by some user
-interface). So changes should be incremental --- adding or deleting
+interface).  So changes should be incremental --- adding or deleting
 modes relative to the current value.
 
 Any \ML{} string is a legal print mode identifier, without any
@@ -678,7 +678,7 @@
 \texttt{symbols}, \texttt{latex}, \texttt{xterm}.
 
 There is a separate table of mixfix productions for pretty printing
-associated with each print mode. The currently active ones are
+associated with each print mode.  The currently active ones are
 conceptually just concatenated from left to right, with the standard
 syntax output table always coming last as default.  Thus mixfix
 productions of preceding modes in the list may override those of later
@@ -687,7 +687,7 @@
 
 \medskip The canonical application of print modes is optional printing
 of mathematical symbols from a special screen font instead of {\sc
-  ascii}. Another example is to re-use Isabelle's advanced
+  ascii}.  Another example is to re-use Isabelle's advanced
 $\lambda$-term printing mechanisms to generate completely different
 output, say for interfacing external tools like \rmindex{model
   checkers} (see also \texttt{HOL/Modelcheck}).
@@ -700,21 +700,21 @@
 
 To keep the grammar small and allow common productions to be shared
 all logical types (except {\tt prop}) are internally represented
-by one nonterminal, namely {\tt logic}. This and omitted or too freely
+by one nonterminal, namely {\tt logic}.  This and omitted or too freely
 chosen priorities may lead to ways of parsing an expression that were
-not intended by the theory's maker. In most cases Isabelle is able to
+not intended by the theory's maker.  In most cases Isabelle is able to
 select one of multiple parse trees that an expression has lead
-to by checking which of them can be typed correctly. But this may not
+to by checking which of them can be typed correctly.  But this may not
 work in every case and always slows down parsing.
 The warning and error messages that can be produced during this process are
 as follows:
 
 If an ambiguity can be resolved by type inference the following
 warning is shown to remind the user that parsing is (unnecessarily)
-slowed down. In cases where it's not easily possible to eliminate the
+slowed down.  In cases where it's not easily possible to eliminate the
 ambiguity the frequency of the warning can be controlled by changing
 the value of {\tt Syntax.ambiguity_level} which has type {\tt int
-ref}. Its default value is 1 and by increasing it one can control how
+ref}.  Its default value is 1 and by increasing it one can control how
 many parse trees are necessary to generate the warning.
 
 \begin{ttbox}
@@ -738,7 +738,7 @@
 
 Ambiguities occuring in syntax translation rules cannot be resolved by
 type inference because it is not necessary for these rules to be type
-correct. Therefore Isabelle always generates an error message and the
+correct.  Therefore Isabelle always generates an error message and the
 ambiguity should be eliminated by changing the grammar or the rule.