28 } |
28 } |
29 \isamarkuptrue% |
29 \isamarkuptrue% |
30 % |
30 % |
31 \begin{isamarkuptext}% |
31 \begin{isamarkuptext}% |
32 \begin{matharray}{rcl} |
32 \begin{matharray}{rcl} |
33 \indexdef{HOLCF}{command}{consts}\mbox{\isa{\isacommand{consts}}} & : & \isartrans{theory}{theory} \\ |
33 \indexdef{HOLCF}{command}{consts}\hypertarget{command.HOLCF.consts}{\hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isartrans{theory}{theory} \\ |
34 \end{matharray} |
34 \end{matharray} |
35 |
35 |
36 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}}. |
36 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}}. |
37 Isabelle mixfix syntax normally refers directly to the pure |
37 Isabelle mixfix syntax normally refers directly to the pure |
38 meta-level function type \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}{\isachardoublequote}}, with application \isa{{\isachardoublequote}f\ x{\isachardoublequote}}. |
38 meta-level function type \isa{{\isachardoublequote}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}{\isachardoublequote}}, with application \isa{{\isachardoublequote}f\ x{\isachardoublequote}}. |
39 |
39 |
40 The HOLCF variant of \mbox{\isa{\isacommand{consts}}} modifies that of |
40 The HOLCF variant of \hyperlink{command.HOLCF.consts}{\mbox{\isa{\isacommand{consts}}}} modifies that of |
41 Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations |
41 Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations |
42 involving continuous function types are treated specifically. Any |
42 involving continuous function types are treated specifically. Any |
43 given syntax template is transformed internally, generating |
43 given syntax template is transformed internally, generating |
44 translation rules for the abstract and concrete representation of |
44 translation rules for the abstract and concrete representation of |
45 continuous application. Note that mixing of HOLCF and Pure |
45 continuous application. Note that mixing of HOLCF and Pure |