1.1 --- a/doc-src/IsarRef/pure.tex	Mon Mar 04 19:08:15 2002 +0100
     1.2 +++ b/doc-src/IsarRef/pure.tex	Mon Mar 04 22:31:21 2002 +0100
     1.3 @@ -754,22 +754,22 @@
     1.4  (\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
     1.5    \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
     1.6  
     1.7 -Claims at the theory level may be either in ``short'' or ``long'' form.  A
     1.8 -short goal merely consists of several simultaneous propositions (often just
     1.9 -one).  A long goal includes an explicit context specification for the
    1.10 -subsequent conclusions, involving local parameters; here the role of each part
    1.11 -of the statement is explicitly marked by separate keywords (see also
    1.12 +Claims at the theory level may be either in short or long form.  A short goal
    1.13 +merely consists of several simultaneous propositions (often just one).  A long
    1.14 +goal includes an explicit context specification for the subsequent
    1.15 +conclusions, involving local parameters; here the role of each part of the
    1.16 +statement is explicitly marked by separate keywords (see also
    1.17  \S\ref{sec:locale}).
    1.18  
    1.19  \begin{rail}
    1.20 -  ('lemma' | 'theorem' | 'corollary') locale? (shortgoal | longgoal)
    1.21 +  ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
    1.22    ;
    1.23 -  ('have' | 'show' | 'hence' | 'thus') shortgoal
    1.24 +  ('have' | 'show' | 'hence' | 'thus') goal
    1.25    ;
    1.26    
    1.27 -  shortgoal: (props + 'and')
    1.28 +  goal: (props + 'and')
    1.29    ;
    1.30 -  longgoal: thmdecl? (contextelem *) 'shows' shortgoal
    1.31 +  longgoal: thmdecl? (contextelem *) 'shows' goal
    1.32    ;
    1.33  \end{rail}
    1.34