--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 23 20:40:20 2012 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 23 21:15:11 2012 +0100
@@ -1648,7 +1648,7 @@
\end{matharray}
@{rail "
- @@{command (HOL) value} ( '[' name ']' )? modes? @{syntax term}
+ @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
;
@@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
@@ -1662,11 +1662,11 @@
@@{command (HOL) nitpick_params}) ( '[' args ']' )?
;
- @@{command (HOL) quickcheck_generator} typeconstructor \\
+ @@{command (HOL) quickcheck_generator} @{syntax nameref} \\
'operations:' ( @{syntax term} +)
;
- @@{command (HOL) find_unused_assms} theoryname?
+ @@{command (HOL) find_unused_assms} @{syntax name}?
;
modes: '(' (@{syntax name} +) ')'
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 23 20:40:20 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 23 21:15:11 2012 +0100
@@ -2351,7 +2351,7 @@
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
-\rail@nont{\isa{name}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
\rail@endbar
\rail@bar
@@ -2408,7 +2408,7 @@
\rail@end
\rail@begin{4}{}
\rail@term{\hyperlink{command.HOL.quickcheck-generator}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}generator}}}}}[]
-\rail@nont{\isa{typeconstructor}}[]
+\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@cr{2}
\rail@term{\isa{operations{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@plus
@@ -2420,7 +2420,7 @@
\rail@term{\hyperlink{command.HOL.find-unused-assms}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}unused{\isaliteral{5F}{\isacharunderscore}}assms}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{theoryname}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endbar
\rail@end
\rail@begin{2}{\isa{modes}}