--- a/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Thu May 15 17:37:21 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOLCF_Specific.tex Thu May 15 17:39:20 2008 +0200
@@ -30,14 +30,14 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{HOLCF}{command}{consts}\mbox{\isa{\isacommand{consts}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
HOLCF provides a separate type for continuous functions \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}{\isachardoublequote}}, with an explicit application operator \isa{{\isachardoublequote}f\ {\isasymcdot}\ x{\isachardoublequote}}.
Isabelle mixfix syntax normally refers directly to the pure
meta-level function type \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}{\isachardoublequote}}, with application \isa{{\isachardoublequote}f\ x{\isachardoublequote}}.
- The HOLCF variant of \mbox{\isa{\isacommand{consts}}} modifies that of
+ The HOLCF variant of \hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}} modifies that of
Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
involving continuous function types are treated specifically. Any
given syntax template is transformed internally, generating
@@ -53,7 +53,7 @@
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{HOLCF}{command}{domain}\mbox{\isa{\isacommand{domain}}} & : & \isartrans{theory}{theory} \\
+ \indexdef{HOLCF}{command}{domain}\hypertarget{command.HOLCF.domain}{\hyperlink{command.HOLCF.domain}{\mbox{\isa{\isacommand{domain}}}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
\begin{rail}