1.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Aug 11 20:32:44 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Aug 12 17:01:30 2011 +0200
     1.3 @@ -1594,11 +1594,24 @@
     1.4  \rail@nont{\isa{attributes}}[]
     1.5  \rail@endbar
     1.6  \rail@end
     1.7 -\rail@begin{2}{}
     1.8 +\rail@begin{5}{}
     1.9  \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
    1.10  \rail@plus
    1.11  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    1.12 -\rail@nextplus{1}
    1.13 +\rail@bar
    1.14 +\rail@nextbar{1}
    1.15 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
    1.16 +\rail@plus
    1.17 +\rail@bar
    1.18 +\rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
    1.19 +\rail@nextbar{2}
    1.20 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    1.21 +\rail@endbar
    1.22 +\rail@nextplus{3}
    1.23 +\rail@endplus
    1.24 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
    1.25 +\rail@endbar
    1.26 +\rail@nextplus{4}
    1.27  \rail@endplus
    1.28  \rail@end
    1.29  \rail@begin{2}{}
    1.30 @@ -1642,7 +1655,10 @@
    1.31    
    1.32    \item \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares names for
    1.33    the local contexts of premises of a theorem; \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}}
    1.34 -  refers to the \emph{suffix} of the list of premises.
    1.35 +  refers to the \emph{prefix} of the list of premises. Each of the
    1.36 +  cases \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} can be of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5B}{\isacharbrackleft}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} where
    1.37 +  the \isa{{\isaliteral{22}{\isachardoublequote}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are the names of the hypotheses in case \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}
    1.38 +  from left to right.
    1.39    
    1.40    \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares
    1.41    names for the conclusions of a named premise \isa{c}; here \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} refers to the prefix of arguments of a logical formula