doc-src/TutorialI/Types/Records.thy

   Record types are not primitive in Isabelle and have a delicate
   internal representation \cite{NaraschewskiW-TPHOLs98}, based on
   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 =
   Xcoord :: int
   Ycoord :: int

 
 text {*
   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
   pt2 :: "\<lparr>Xcoord :: int, Ycoord :: int\<rparr>"
   "pt2 \<equiv> \<lparr>Xcoord = -45, Ycoord = 97\<rparr>"

 lemma "point.more cpt1 = \<lparr>col = Green\<rparr>"
   by (simp add: cpt1_def)
 
 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}.
 
   To define generic operations, we need to know a bit more about

   of the original record type) and returns a fixed record, removing
   any additional fields.
 
   \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
   point.defs}, @{text cpoint.defs}, etc.).