--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu May 05 23:23:02 2011 +0200
@@ -304,7 +304,7 @@
@{syntax_def typespec}:
(() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
;
- @{syntax_def typespecsorts}:
+ @{syntax_def typespec_sorts}:
(() | (@{syntax typefree} ('::' @{syntax sort})?) |
'(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
"}
@@ -319,9 +319,9 @@
This works both for @{syntax term} and @{syntax prop}.
@{rail "
- @{syntax_def termpat}: '(' (@'is' @{syntax term} +) ')'
+ @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
;
- @{syntax_def proppat}: '(' (@'is' @{syntax prop} +) ')'
+ @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
"}
\medskip Declarations of local variables @{text "x :: \<tau>"} and
@@ -335,7 +335,7 @@
@{rail "
@{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
;
- @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax proppat}? +)
+ @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
"}
The treatment of multiple declarations corresponds to the