HOL record: explicitly allow sort constraints;
authorwenzelm
Thu Apr 15 20:56:04 2010 +0200 (2010-04-15)
changeset 36158d2ad76e374d3
parent 36157 2fb3e278a5d7
child 36159 bffb04bf4e83
HOL record: explicitly allow sort constraints;
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     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