1.1 --- a/doc-src/IsarRef/syntax.tex	Wed Sep 01 21:26:26 1999 +0200
     1.2 +++ b/doc-src/IsarRef/syntax.tex	Wed Sep 01 21:28:42 1999 +0200
     1.3 @@ -265,16 +265,16 @@
     1.4  
     1.5  Proof methods are either basic ones, or expressions composed of methods via
     1.6  ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
     1.7 -``\texttt{?}'' (try), ``\texttt{*}'' (repeat ${} \ge 0$ times), ``\texttt{+}''
     1.8 -(repeat ${} > 0$ times).  In practice, proof methods are usually just a comma
     1.9 -separated list of \railqtoken{nameref}~\railnonterm{args} specifications.
    1.10 -Thus the syntax is similar to that of attributes, with plain parentheses
    1.11 -instead of square brackets.  Note that parentheses may be dropped for single
    1.12 -method specifications without arguments.
    1.13 +``\texttt{?}'' (try), ``\texttt{+}'' (at least once).  In practice, proof
    1.14 +methods are usually just a comma separated list of
    1.15 +\railqtoken{nameref}~\railnonterm{args} specifications.  Thus the syntax is
    1.16 +similar to that of attributes, with plain parentheses instead of square
    1.17 +brackets.  Note that parentheses may be dropped for single method
    1.18 +specifications without arguments.
    1.19  
    1.20  \indexouternonterm{method}
    1.21  \begin{rail}
    1.22 -  method: (nameref | '(' methods ')') (() | '?' | '*' | '+')
    1.23 +  method: (nameref | '(' methods ')') (() | '?' | '+')
    1.24    ;
    1.25    methods: (nameref args | method) + (',' | '|')
    1.26    ;