# HG changeset patch
# User wenzelm
# Date 1445442806 -7200
# Node ID 4efe9a6dd212e97f7423d12fa65b9ed37248b554
# Parent  32a20d7b3ee451ef2596b9026ad6b5e9b5d0f9c5
tuned document;

diff -r 32a20d7b3ee4 -r 4efe9a6dd212 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Wed Oct 21 17:21:38 2015 +0200
+++ b/src/HOL/ex/Records.thy	Wed Oct 21 17:53:26 2015 +0200
@@ -32,8 +32,8 @@
 
   \medskip Record declarations define new types and type abbreviations:
   @{text [display]
-"  point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
-  'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type"}
+\<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type
+'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr>  = 'a point_ext_type\<close>}
 \<close>
 
 consts foo2 :: "(| xpos :: nat, ypos :: nat |)"
@@ -173,12 +173,12 @@
 
 
 text \<open>
-  The record declaration defines a new type constructure and abbreviations:
+  The record declaration defines a new type constructor and abbreviations:
   @{text [display]
-"  cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
-     () cpoint_ext_type point_ext_type
-   'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
-     'a cpoint_ext_type point_ext_type"}
+\<open>cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) =
+  () cpoint_ext_type point_ext_type
+'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) =
+  'a cpoint_ext_type point_ext_type\<close>}
 \<close>
 
 consts foo6 :: cpoint