1.1 --- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed May 07 12:38:55 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed May 07 12:56:11 2008 +0200
     1.3 @@ -4,4 +4,56 @@
     1.4  imports HOLCF
     1.5  begin
     1.6  
     1.7 +chapter {* HOLCF specific elements *}
     1.8 +
     1.9 +section {* Mixfix syntax for continuous operations *}
    1.10 +
    1.11 +text {*
    1.12 +  \begin{matharray}{rcl}
    1.13 +    @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
    1.14 +  \end{matharray}
    1.15 +
    1.16 +  HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
    1.17 +  \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
    1.18 +  Isabelle mixfix syntax normally refers directly to the pure
    1.19 +  meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
    1.20 +  x"}.
    1.21 +
    1.22 +  The HOLCF variant of @{command (HOLCF) "consts"} modifies that of
    1.23 +  Pure Isabelle (cf.\ \secref{sec:consts}) such that declarations
    1.24 +  involving continuous function types are treated specifically.  Any
    1.25 +  given syntax template is transformed internally, generating
    1.26 +  translation rules for the abstract and concrete representation of
    1.27 +  continuous application.  Note that mixing of HOLCF and Pure
    1.28 +  application is \emph{not} supported!
    1.29 +*}
    1.30 +
    1.31 +
    1.32 +section {* Recursive domains *}
    1.33 +
    1.34 +text {*
    1.35 +  \begin{matharray}{rcl}
    1.36 +    @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
    1.37 +  \end{matharray}
    1.38 +
    1.39 +  \begin{rail}
    1.40 +    'domain' parname? (dmspec + 'and')
    1.41 +    ;
    1.42 +
    1.43 +    dmspec: typespec '=' (cons + '|')
    1.44 +    ;
    1.45 +    cons: name (type *) mixfix?
    1.46 +    ;
    1.47 +    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    1.48 +  \end{rail}
    1.49 +
    1.50 +  Recursive domains in HOLCF are analogous to datatypes in classical
    1.51 +  HOL (cf.\ \secref{sec:hol-datatype}).  Mutual recursion is
    1.52 +  supported, but no nesting nor arbitrary branching.  Domain
    1.53 +  constructors may be strict (default) or lazy, the latter admits to
    1.54 +  introduce infinitary objects in the typical LCF manner (e.g.\ lazy
    1.55 +  lists).  See also \cite{MuellerNvOS99} for a general discussion of
    1.56 +  HOLCF domains.
    1.57 +*}
    1.58 +
    1.59  end