--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy Sun May 01 18:57:45 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy Mon May 02 01:05:50 2011 +0200
@@ -34,16 +34,17 @@
@{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
- \begin{rail}
- 'domain' parname? (dmspec + 'and')
+ @{rail "
+ @@{command (HOLCF) domain} @{syntax parname}? (dmspec + @'and')
;
- dmspec: typespec '=' (cons + '|')
+ dmspec: @{syntax typespec} '=' (cons + '|')
+ ;
+ cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
;
- cons: name (type *) mixfix?
- ;
- dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
- \end{rail}
+ 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