--- a/doc-src/IsarRef/Thy/Generic.thy Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Wed Feb 15 21:29:23 2012 +0100
@@ -1226,7 +1226,7 @@
declarations internally.
@{rail "
- @@{command judgment} @{syntax constdecl}
+ @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
;
@@{attribute atomize} ('(' 'full' ')')?
;
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Feb 15 21:29:23 2012 +0100
@@ -864,7 +864,9 @@
@{rail "
@@{command (HOL) record} @{syntax typespec_sorts} '=' \\
- (@{syntax type} '+')? (@{syntax constdecl} +)
+ (@{syntax type} '+')? (constdecl +)
+ ;
+ constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
"}
\begin{description}
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Feb 15 21:29:23 2012 +0100
@@ -1038,12 +1038,14 @@
@{rail "
@@{command nonterminal} (@{syntax name} + @'and')
;
- (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (@{syntax constdecl} +)
+ (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
;
(@@{command translations} | @@{command no_translations})
(transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
;
+ constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
+ ;
mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
;
transpat: ('(' @{syntax nameref} ')')? @{syntax string}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Feb 15 21:29:23 2012 +0100
@@ -1838,9 +1838,15 @@
declarations internally.
\begin{railoutput}
-\rail@begin{1}{}
+\rail@begin{2}{}
\rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
\rail@end
\rail@begin{2}{}
\rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Feb 15 21:29:23 2012 +0100
@@ -1288,10 +1288,19 @@
\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
\rail@endbar
\rail@plus
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\isa{constdecl}}[]
\rail@nextplus{3}
\rail@endplus
\rail@end
+\rail@begin{2}{\isa{constdecl}}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
+\rail@end
\end{railoutput}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 15 21:08:27 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Wed Feb 15 21:29:23 2012 +0100
@@ -1231,7 +1231,7 @@
\rail@nont{\hyperlink{syntax.mode}{\mbox{\isa{mode}}}}[]
\rail@endbar
\rail@plus
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\isa{constdecl}}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
@@ -1260,6 +1260,15 @@
\rail@nextplus{6}
\rail@endplus
\rail@end
+\rail@begin{2}{\isa{constdecl}}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
+\rail@end
\rail@begin{3}{\isa{mode}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@bar