1.1 --- a/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 07 23:56:11 2002 +0100
     1.2 +++ b/doc-src/TutorialI/Types/document/Records.tex	Mon Jan 07 23:56:25 2002 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4    nested copies of the primitive product type.  A \commdx{record}
     1.5    declaration introduces a new record type scheme by specifying its
     1.6    fields, which are packaged internally to hold up the perception of
     1.7 -  the record as a distinguished entity.  Here is a simply example.%
     1.8 +  the record as a distinguished entity.  Here is a very simply example:%
     1.9  \end{isamarkuptext}%
    1.10  \isamarkuptrue%
    1.11  \isacommand{record}\ point\ {\isacharequal}\isanewline
    1.12 @@ -126,16 +126,15 @@
    1.13  \ \ {\isachardoublequote}cpt{\isadigit{1}}\ {\isasymequiv}\ {\isasymlparr}Xcoord\ {\isacharequal}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharcomma}\ Ycoord\ {\isacharequal}\ {\isadigit{2}}{\isadigit{3}}{\isacharcomma}\ col\ {\isacharequal}\ Green{\isasymrparr}{\isachardoublequote}\isamarkupfalse%
    1.14  %
    1.15  \begin{isamarkuptext}%
    1.16 -We can define generic operations that work on arbitrary instances of
    1.17 -  a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any
    1.18 -  further extensions.  Every record structure has an implicit
    1.19 -  pseudo-field, \cdx{more}, that keeps the extension as an explicit
    1.20 -  value.  Its type is declared as completely polymorphic:~\isa{{\isacharprime}a}.
    1.21 -  When a fixed record value is expressed using just its standard
    1.22 -  fields, the value of \isa{more} is implicitly set to \isa{{\isacharparenleft}{\isacharparenright}},
    1.23 -  the empty tuple, which has type \isa{unit}.  Within the record
    1.24 -  brackets, you can refer to the \isa{more} field by writing
    1.25 -  ``\isa{{\isasymdots}}'' (three dots):%
    1.26 +\medskip We can define generic operations that work on arbitrary
    1.27 +  instances of a record scheme, e.g.\ covering \isa{point}, \isa{cpoint}, and any further extensions.  Every record structure has an
    1.28 +  implicit pseudo-field, \cdx{more}, that keeps the extension as an
    1.29 +  explicit value.  Its type is declared as completely
    1.30 +  polymorphic:~\isa{{\isacharprime}a}.  When a fixed record value is expressed
    1.31 +  using just its standard fields, the value of \isa{more} is
    1.32 +  implicitly set to \isa{{\isacharparenleft}{\isacharparenright}}, the empty tuple, which has type
    1.33 +  \isa{unit}.  Within the record brackets, you can refer to the
    1.34 +  \isa{more} field by writing ``\isa{{\isasymdots}}'' (three dots):%
    1.35  \end{isamarkuptext}%
    1.36  \isamarkuptrue%
    1.37  \isacommand{lemma}\ {\isachardoublequote}Xcoord\ {\isasymlparr}Xcoord\ {\isacharequal}\ a{\isacharcomma}\ Ycoord\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ p{\isasymrparr}\ {\isacharequal}\ a{\isachardoublequote}\isanewline
    1.38 @@ -336,8 +335,8 @@
    1.39  The generic cases method does not admit references to locally bound
    1.40    parameters of a goal.  In longer proof scripts one might have to
    1.41    fall back on the primitive \isa{rule{\isacharunderscore}tac} used together with the
    1.42 -  internal field representation rules of records.  E.g.\ the above use
    1.43 -  of \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
    1.44 +  internal field representation rules of records.  The above use of
    1.45 +  \isa{{\isacharparenleft}cases\ r{\isacharparenright}} would become \isa{{\isacharparenleft}rule{\isacharunderscore}tac\ r\ {\isacharequal}\ r\ in\ point{\isachardot}cases{\isacharunderscore}scheme{\isacharparenright}}.%
    1.46  \end{isamarkuptext}%
    1.47  \isamarkuptrue%
    1.48  %