1.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Sun Apr 23 11:41:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Apr 25 08:09:10 2000 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  \noindent\indexbold{*types}%
     1.5  Internally all synonyms are fully expanded.  As a consequence Isabelle's
     1.6  output never contains synonyms.  Their main purpose is to improve the
     1.7 -readability of theory definitions.  Synonyms can be used just like any other
     1.8 +readability of theories.  Synonyms can be used just like any other
     1.9  type:%
    1.10  \end{isamarkuptext}%
    1.11  \isacommand{consts}~nand~::~gate\isanewline
    1.12 @@ -24,7 +24,7 @@
    1.13  \begin{isamarkuptext}%
    1.14  \noindent%
    1.15  where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
    1.16 -\isa{exor_def} are arbitrary user-supplied names.
    1.17 +\isa{exor_def} are user-supplied names.
    1.18  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
    1.19  that should only be used in constant definitions.
    1.20  Declarations and definitions can also be merged%