1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:15:11 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Thu May 05 23:23:02 2011 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4  \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
     1.5  \rail@bar
     1.6  \rail@nextbar{4}
     1.7 -\rail@nont{\hyperlink{syntax.termpat}{\mbox{\isa{termpat}}}}[]
     1.8 +\rail@nont{\hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}}}[]
     1.9  \rail@endbar
    1.10  \rail@end
    1.11  \end{railoutput}
    1.12 @@ -348,8 +348,8 @@
    1.13  \end{railoutput}
    1.14  
    1.15  
    1.16 -  The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.termpat}{\mbox{\isa{termpat}}} or
    1.17 -  \hyperlink{syntax.proppat}{\mbox{\isa{proppat}}} (see \secref{sec:term-decls}).
    1.18 +  The syntax of \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns follows \hyperlink{syntax.term-pat}{\mbox{\isa{term{\isaliteral{5F}{\isacharunderscore}}pat}}} or
    1.19 +  \hyperlink{syntax.prop-pat}{\mbox{\isa{prop{\isaliteral{5F}{\isacharunderscore}}pat}}} (see \secref{sec:term-decls}).
    1.20  
    1.21    \begin{description}
    1.22  
    1.23 @@ -780,7 +780,7 @@
    1.24    all goals, and ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}n{\isaliteral{2D}{\isacharminus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}'' to all goals starting from \isa{{\isaliteral{22}{\isachardoublequote}}n{\isaliteral{22}{\isachardoublequote}}}.
    1.25  
    1.26    \begin{railoutput}
    1.27 -\rail@begin{4}{\indexdef{}{syntax}{goalspec}\hypertarget{syntax.goalspec}{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}}
    1.28 +\rail@begin{4}{\indexdef{}{syntax}{goal\_spec}\hypertarget{syntax.goal-spec}{\hyperlink{syntax.goal-spec}{\mbox{\isa{goal{\isaliteral{5F}{\isacharunderscore}}spec}}}}}
    1.29  \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
    1.30  \rail@bar
    1.31  \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]