--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 07:06:39 2010 -0800
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 24 20:37:01 2010 +0100
@@ -13,14 +13,14 @@
\end{matharray}
\begin{rail}
- 'typedecl' typespec infix?
+ 'typedecl' typespec mixfix?
;
'typedef' altname? abstype '=' repset
;
altname: '(' (name | 'open' | 'open' name) ')'
;
- abstype: typespec infix?
+ abstype: typespec mixfix?
;
repset: term ('morphisms' name name)?
;
@@ -367,7 +367,7 @@
'rep\_datatype' ('(' (name +) ')')? (term +)
;
- dtspec: parname? typespec infix? '=' (cons + '|')
+ dtspec: parname? typespec mixfix? '=' (cons + '|')
;
cons: name ( type * ) mixfix?
\end{rail}