# HG changeset patch
# User paulson
# Date 1010665548 -3600
# Node ID f0d09c9693d680f39576331f80a9f71f8099fef0
# Parent  deae8004552756333c978ad788b2424beecaaab0
stylistic changes

diff -r deae80045527 -r f0d09c9693d6 doc-src/TutorialI/Types/Records.thy
--- 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
diff -r deae80045527 -r f0d09c9693d6 doc-src/TutorialI/Types/document/Records.tex
--- 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.).