# HG changeset patch # User wenzelm # Date 1271357764 -7200 # Node ID d2ad76e374d3a86c1a6478321a63322052a23910 # Parent 2fb3e278a5d7282d78d13eed881a62c564d76978 HOL record: explicitly allow sort constraints; diff -r 2fb3e278a5d7 -r d2ad76e374d3 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Apr 15 20:37:27 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Apr 15 20:56:04 2010 +0200 @@ -178,7 +178,7 @@ \end{matharray} \begin{rail} - 'record' typespec '=' (type '+')? (constdecl +) + 'record' typespecsorts '=' (type '+')? (constdecl +) ; \end{rail} diff -r 2fb3e278a5d7 -r d2ad76e374d3 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Apr 15 20:37:27 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Apr 15 20:56:04 2010 +0200 @@ -202,7 +202,7 @@ \end{matharray} \begin{rail} - 'record' typespec '=' (type '+')? (constdecl +) + 'record' typespecsorts '=' (type '+')? (constdecl +) ; \end{rail}