--- 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.).