# HG changeset patch
# User wenzelm
# Date 1210157771 -7200
# Node ID 6ac51a2f48e1377ce63f7d71f911003b28ff291f
# Parent  ec46381f149df17e5161eb80b72e9895fe0649ba
converted HOLCF specific elements;

diff -r ec46381f149d -r 6ac51a2f48e1 doc-src/IsarRef/Thy/HOLCF_Specific.thy
--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed May 07 12:38:55 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy	Wed May 07 12:56:11 2008 +0200
@@ -4,4 +4,56 @@
 imports HOLCF
 begin
 
+chapter {* HOLCF specific elements *}
+
+section {* Mixfix syntax for continuous operations *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{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"} & : & \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.\ \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
diff -r ec46381f149d -r 6ac51a2f48e1 doc-src/IsarRef/logics.tex
--- 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}