doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 43576 528a2ba8fa74
parent 43575 3f19e324ff59
child 43881 665623e695ea
child 44111 dfd4ef8e73f6
     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}