# HG changeset patch
# User haftmann
# Date 1294751653 -3600
# Node ID 4c717333b0cc68033e9aada14f4dcbcf81111f3b
# Parent  6d19301074cf771cc16c32b83b7ed075181a25ab
tuned text

diff -r 6d19301074cf -r 4c717333b0cc doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jan 11 14:12:37 2011 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jan 11 14:14:13 2011 +0100
@@ -399,11 +399,11 @@
   \begin{description}
 
   \item @{command (HOL) "enriched_type"} allows to prove and register
-  properties about type constructors which refer to their functorial
-  structure; these properties then can be used by other packages to
+  properties about the functorial structure of type constructors;
+  these properties then can be used by other packages to
   deal with those type constructors in certain type constructions.
   Characteristic theorems are noted in the current local theory; by
-  default, they are prefixed with base name of the type constructor,
+  default, they are prefixed with the base name of the type constructor,
   an explicit prefix can be given alternatively.
 
   The given term @{text "m"} is considered as \emph{mapper} for the
diff -r 6d19301074cf -r 4c717333b0cc doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jan 11 14:12:37 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jan 11 14:14:13 2011 +0100
@@ -399,7 +399,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{HOL}{command}{type\_lifting}\hypertarget{command.HOL.type-lifting}{\hyperlink{command.HOL.type-lifting}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}lifting}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
+    \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
   \end{matharray}
 
   \begin{rail}
@@ -409,12 +409,12 @@
 
   \begin{description}
 
-  \item \hyperlink{command.HOL.type-lifting}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}lifting}}}} allows to prove and register
-  properties about type constructors which refer to their functorial
-  structure; these properties then can be used by other packages to
+  \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register
+  properties about the functorial structure of type constructors;
+  these properties then can be used by other packages to
   deal with those type constructors in certain type constructions.
   Characteristic theorems are noted in the current local theory; by
-  default, they are prefixed with base name of the type constructor,
+  default, they are prefixed with the base name of the type constructor,
   an explicit prefix can be given alternatively.
 
   The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the