--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy Tue Aug 28 12:22:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-theory HOLCF_Specific
-imports Base HOLCF
-begin
-
-chapter {* Isabelle/HOLCF \label{ch:holcf} *}
-
-section {* Mixfix syntax for continuous operations *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
- \<beta>"}, with an explicit application operator @{term "f \<cdot> x"}.
- Isabelle mixfix syntax normally refers directly to the pure
- meta-level function type @{text "\<alpha> \<Rightarrow> \<beta>"}, with application @{text "f
- x"}.
-
- The HOLCF variant of @{command (HOLCF) "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
- translation rules for the abstract and concrete representation of
- continuous application. Note that mixing of HOLCF and Pure
- application is \emph{not} supported!
-*}
-
-
-section {* Recursive domains *}
-
-text {*
- \begin{matharray}{rcl}
- @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
- \end{matharray}
-
- @{rail "
- @@{command (HOLCF) domain} @{syntax parname}? (spec + @'and')
- ;
-
- spec: @{syntax typespec} '=' (cons + '|')
- ;
- cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
- ;
- dtrules: @'distinct' @{syntax thmrefs} @'inject' @{syntax thmrefs}
- @'induction' @{syntax thmrefs}
- "}
-
- Recursive domains in HOLCF are analogous to datatypes in classical
- HOL (cf.\ \secref{sec:hol-datatype}). Mutual recursion is
- supported, but no nesting nor arbitrary branching. Domain
- constructors may be strict (default) or lazy, the latter admits to
- introduce infinitary objects in the typical LCF manner (e.g.\ lazy
- lists). See also \cite{MuellerNvOS99} for a general discussion of
- HOLCF domains.
-*}
-
-end