1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 05 23:15:11 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 05 23:23:02 2011 +0200
1.3 @@ -55,7 +55,7 @@
1.4 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1.5 \rail@end
1.6 \rail@begin{2}{\isa{abstype}}
1.7 -\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
1.8 +\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.9 \rail@bar
1.10 \rail@nextbar{1}
1.11 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.12 @@ -239,7 +239,7 @@
1.13 \begin{railoutput}
1.14 \rail@begin{4}{}
1.15 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
1.16 -\rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
1.17 +\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
1.18 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.19 \rail@cr{2}
1.20 \rail@bar
1.21 @@ -1604,7 +1604,7 @@
1.22 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.23 \rail@bar
1.24 \rail@nextbar{1}
1.25 -\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1.26 +\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
1.27 \rail@endbar
1.28 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.29 \rail@bar
1.30 @@ -1616,7 +1616,7 @@
1.31 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1.32 \rail@bar
1.33 \rail@nextbar{1}
1.34 -\rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1.35 +\rail@nont{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}[]
1.36 \rail@endbar
1.37 \rail@bar
1.38 \rail@nextbar{1}