--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 05 23:15:11 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 05 23:23:02 2011 +0200
@@ -55,7 +55,7 @@
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
\rail@begin{2}{\isa{abstype}}
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
@@ -239,7 +239,7 @@
\begin{railoutput}
\rail@begin{4}{}
\rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
-\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
+\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
\rail@cr{2}
\rail@bar
@@ -1604,7 +1604,7 @@
\rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@bar
@@ -1616,7 +1616,7 @@
\rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
+\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}