1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jan 11 14:12:37 2011 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jan 11 14:14:13 2011 +0100
     1.3 @@ -399,11 +399,11 @@
     1.4    \begin{description}
     1.5  
     1.6    \item @{command (HOL) "enriched_type"} allows to prove and register
     1.7 -  properties about type constructors which refer to their functorial
     1.8 -  structure; these properties then can be used by other packages to
     1.9 +  properties about the functorial structure of type constructors;
    1.10 +  these properties then can be used by other packages to
    1.11    deal with those type constructors in certain type constructions.
    1.12    Characteristic theorems are noted in the current local theory; by
    1.13 -  default, they are prefixed with base name of the type constructor,
    1.14 +  default, they are prefixed with the base name of the type constructor,
    1.15    an explicit prefix can be given alternatively.
    1.16  
    1.17    The given term @{text "m"} is considered as \emph{mapper} for the

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jan 11 14:12:37 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jan 11 14:14:13 2011 +0100
     2.3 @@ -399,7 +399,7 @@
     2.4  %
     2.5  \begin{isamarkuptext}%
     2.6  \begin{matharray}{rcl}
     2.7 -    \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}}}
     2.8 +    \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}}}
     2.9    \end{matharray}
    2.10  
    2.11    \begin{rail}
    2.12 @@ -409,12 +409,12 @@
    2.13  
    2.14    \begin{description}
    2.15  
    2.16 -  \item \hyperlink{command.HOL.type-lifting}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}lifting}}}} allows to prove and register
    2.17 -  properties about type constructors which refer to their functorial
    2.18 -  structure; these properties then can be used by other packages to
    2.19 +  \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register
    2.20 +  properties about the functorial structure of type constructors;
    2.21 +  these properties then can be used by other packages to
    2.22    deal with those type constructors in certain type constructions.
    2.23    Characteristic theorems are noted in the current local theory; by
    2.24 -  default, they are prefixed with base name of the type constructor,
    2.25 +  default, they are prefixed with the base name of the type constructor,
    2.26    an explicit prefix can be given alternatively.
    2.27  
    2.28    The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the