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.
allow sort constraints in HOL/typedef;
authorwenzelm
Fri, 19 Mar 2010 00:46:08 +0100
changeset 35841 94f901e4969a
parent 35840 01d7c4ba9050
child 35842 7c170d39a808
allow sort constraints in HOL/typedef;
doc-src/IsarRef/Thy/HOL_Specific.thy file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/Outer_Syntax.thy file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/document/HOL_Specific.tex file | annotate | diff | comparison | revisions
doc-src/IsarRef/Thy/document/Outer_Syntax.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Mar 19 00:46:08 2010 +0100
@@ -17,7 +17,7 @@
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec mixfix?
+    abstype: typespecsorts mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Fri Mar 19 00:46:08 2010 +0100
@@ -297,9 +297,13 @@
   only plain postfix notation is available here, but no infixes.
 
   \indexouternonterm{typespec}
+  \indexouternonterm{typespecsorts}
   \begin{rail}
     typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
     ;
+
+    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
+    ;
   \end{rail}
 *}
 
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Mar 19 00:46:08 2010 +0100
@@ -37,7 +37,7 @@
 
     altname: '(' (name | 'open' | 'open' name) ')'
     ;
-    abstype: typespec mixfix?
+    abstype: typespecsorts mixfix?
     ;
     repset: term ('morphisms' name name)?
     ;
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:43:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Fri Mar 19 00:46:08 2010 +0100
@@ -320,9 +320,13 @@
   only plain postfix notation is available here, but no infixes.
 
   \indexouternonterm{typespec}
+  \indexouternonterm{typespecsorts}
   \begin{rail}
     typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
     ;
+
+    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
+    ;
   \end{rail}%
 \end{isamarkuptext}%
 \isamarkuptrue%
isabelle