--- a/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu Nov 13 21:43:46 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOLCF_Specific.thy Thu Nov 13 21:45:40 2008 +0100
@@ -10,7 +10,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOLCF) "consts"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOLCF) "consts"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
HOLCF provides a separate type for continuous functions @{text "\<alpha> \<rightarrow>
@@ -33,7 +33,7 @@
text {*
\begin{matharray}{rcl}
- @{command_def (HOLCF) "domain"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOLCF) "domain"} & : & @{text "theory \<rightarrow> theory"} \\
\end{matharray}
\begin{rail}