Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOL record: explicitly allow sort constraints;
authorwenzelm
Thu, 15 Apr 2010 20:56:04 +0200
changeset 36158 d2ad76e374d3
parent 36157 2fb3e278a5d7
child 36159 bffb04bf4e83
HOL record: explicitly allow sort constraints;
doc-src/IsarRef/Thy/HOL_Specific.thy file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/document/HOL_Specific.tex file | annotate | diff | comparison | revisions 
--- 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}
 
--- 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}
isabelle