author paulson Thu, 10 Jan 2002 13:25:48 +0100 changeset 12700 f0d09c9693d6 parent 12699 deae80045527 child 12701 77ac6d8451ea
stylistic changes
--- a/doc-src/TutorialI/Types/Records.thy	Thu Jan 10 11:22:03 2002 +0100
+++ b/doc-src/TutorialI/Types/Records.thy	Thu Jan 10 13:25:48 2002 +0100
@@ -37,7 +37,7 @@
nested copies of the primitive product type.  A \commdx{record}
declaration introduces a new record type scheme by specifying its
fields, which are packaged internally to hold up the perception of
-  the record as a distinguished entity.  Here is a very simply example:
+  the record as a distinguished entity.  Here is a simple example:
*}

record point =
@@ -58,7 +58,7 @@
We see above the ASCII notation for record brackets.  You can also
use the symbolic brackets @{text \<lparr>} and @{text \<rparr>}.  Record type
expressions can be also written directly with individual fields.
-  The type name above is merely an abbreviations.
+  The type name above is merely an abbreviation.
*}

constdefs
@@ -152,7 +152,7 @@

text {*
We see that the colour part attached to this @{typ point} is a
-  (rudimentary) record in its own right, namely @{text "\<lparr>col =
+  rudimentary record in its own right, namely @{text "\<lparr>col =
Green\<rparr>"}.  In order to select or update @{text col}, this fragment
needs to be put back into the context of the parent type scheme, say
as @{text more} part of another @{typ point}.
@@ -345,7 +345,7 @@

\end{itemize}

-  These functions merely provide handsome abbreviations for standard
+  These functions provide useful abbreviations for standard
record expressions involving constructors and selectors.  The
definitions, which are \emph{not} unfolded by default, are made
available by the collective name of @{text defs} (@{text
--- a/doc-src/TutorialI/Types/document/Records.tex	Thu Jan 10 11:22:03 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex	Thu Jan 10 13:25:48 2002 +0100
@@ -41,7 +41,7 @@
nested copies of the primitive product type.  A \commdx{record}
declaration introduces a new record type scheme by specifying its
fields, which are packaged internally to hold up the perception of
-  the record as a distinguished entity.  Here is a very simply example:%
+  the record as a distinguished entity.  Here is a simple example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{record}\ point\ {\isacharequal}\isanewline
@@ -62,7 +62,7 @@
We see above the ASCII notation for record brackets.  You can also
use the symbolic brackets \isa{{\isasymlparr}} and \isa{{\isasymrparr}}.  Record type
expressions can be also written directly with individual fields.
-  The type name above is merely an abbreviations.%
+  The type name above is merely an abbreviation.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{constdefs}\isanewline
@@ -156,7 +156,7 @@
%
\begin{isamarkuptext}%
We see that the colour part attached to this \isa{point} is a
-  (rudimentary) record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
+  rudimentary record in its own right, namely \isa{{\isasymlparr}col\ {\isacharequal}\ Green{\isasymrparr}}.  In order to select or update \isa{col}, this fragment
needs to be put back into the context of the parent type scheme, say
as \isa{more} part of another \isa{point}.

@@ -369,7 +369,7 @@

\end{itemize}

-  These functions merely provide handsome abbreviations for standard
+  These functions provide useful abbreviations for standard
record expressions involving constructors and selectors.  The
definitions, which are \emph{not} unfolded by default, are made
available by the collective name of \isa{defs} (\isa{point{\isachardot}defs}, \isa{cpoint{\isachardot}defs}, etc.).