--- a/doc-src/IsarRef/logics.tex Wed May 07 12:38:55 2008 +0200
+++ b/doc-src/IsarRef/logics.tex Wed May 07 12:56:11 2008 +0200
@@ -1048,53 +1048,6 @@
\end{descr}
-\section{HOLCF}
-
-\subsection{Mixfix syntax for continuous operations}
-
-\indexisarcmdof{HOLCF}{consts}
-
-\begin{matharray}{rcl}
- \isarcmd{consts} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-HOLCF provides a separate type for continuous functions $\alpha \to
-\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix
-syntax normally refers directly to the pure meta-level function type $\alpha
-\To \beta$, with application $f\,x$.
-
-The HOLCF variant of $\CONSTS$ modifies that of Pure Isabelle (cf.\
-\S\ref{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!
-
-\subsection{Recursive domains}
-
-\indexisarcmdof{HOLCF}{domain}
-\begin{matharray}{rcl}
- \isarcmd{domain} & : & \isartrans{theory}{theory} \\
-\end{matharray}
-
-\begin{rail}
- 'domain' parname? (dmspec + 'and')
- ;
-
- dmspec: typespec '=' (cons + '|')
- ;
- cons: name (type *) mixfix?
- ;
- dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
-\end{rail}
-
-Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
-\S\ref{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.
-
\section{ZF}