diff -r d54a3d39ba85 -r c04001b3a753 doc-src/IsarRef/Thy/HOLCF_Specific.thy
--- 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