1.1 --- a/doc-src/Ref/defining.tex	Tue Jan 18 11:00:10 2000 +0100
     1.2 +++ b/doc-src/Ref/defining.tex	Tue Jan 18 11:33:31 2000 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4       &$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\
     1.5       &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\
     1.6  $sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~
     1.7 -  {\tt\ttlbrace} $id$ ~$|$~ $longid$ {\tt,} \dots {\tt,} $id$ ~$|$~ $longid$ {\tt\ttrbrace}
     1.8 +  {\tt\ttlbrace} $id$ ~$|$~ $longid${\tt,}\dots{\tt,} $id$ ~$|$~$longid$ {\tt\ttrbrace}
     1.9  \end{tabular}
    1.10  \index{*PROP symbol}
    1.11  \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
    1.12 @@ -291,8 +291,8 @@
    1.13  \item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
    1.14    theory~{\it thy} as an \ML\ value.
    1.15  
    1.16 -\item[\ttindexbold{print_syntax} $thy$] displays the syntax part of $thy$
    1.17 -  using {\tt Syntax.print_syntax}.
    1.18 +\item[\ttindexbold{print_syntax} $thy$] uses {\tt Syntax.print_syntax}
    1.19 + to display the syntax part of theory $thy$.
    1.20  
    1.21  \item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
    1.22    information contained in the syntax {\it syn}.  The displayed output can
    1.23 @@ -508,7 +508,7 @@
    1.24    "-" :: exp => exp          ("- _"    [3] 3)
    1.25  end
    1.26  \end{ttbox}
    1.27 -If you put this into a file {\tt ExpSyntax.thy} and load it via {\tt
    1.28 +If you put this into a file {\tt ExpSyntax.thy} and load it by {\tt
    1.29    use_thy"ExpSyntax"}, you can run some tests:
    1.30  \begin{ttbox}
    1.31  val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp";