1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Apr 15 20:37:27 2010 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Apr 15 20:56:04 2010 +0200
1.3 @@ -178,7 +178,7 @@
1.4 \end{matharray}
1.5
1.6 \begin{rail}
1.7 - 'record' typespec '=' (type '+')? (constdecl +)
1.8 + 'record' typespecsorts '=' (type '+')? (constdecl +)
1.9 ;
1.10 \end{rail}
1.11
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Apr 15 20:37:27 2010 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Apr 15 20:56:04 2010 +0200
2.3 @@ -202,7 +202,7 @@
2.4 \end{matharray}
2.5
2.6 \begin{rail}
2.7 - 'record' typespec '=' (type '+')? (constdecl +)
2.8 + 'record' typespecsorts '=' (type '+')? (constdecl +)
2.9 ;
2.10 \end{rail}
2.11