# HG changeset patch
# User wenzelm
# Date 936214122 -7200
# Node ID 6ea8cbf94118ef39ebb1a540bca55cf5af9a815a
# Parent  8f284fbb8728f559525092e7bd70137657ce0166
removed "*" method combinator;

diff -r 8f284fbb8728 -r 6ea8cbf94118 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed Sep 01 21:26:26 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Wed Sep 01 21:28:42 1999 +0200
@@ -265,16 +265,16 @@
 
 Proof methods are either basic ones, or expressions composed of methods via
 ``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
-``\texttt{?}'' (try), ``\texttt{*}'' (repeat ${} \ge 0$ times), ``\texttt{+}''
-(repeat ${} > 0$ times).  In practice, proof methods are usually just a comma
-separated list of \railqtoken{nameref}~\railnonterm{args} specifications.
-Thus the syntax is similar to that of attributes, with plain parentheses
-instead of square brackets.  Note that parentheses may be dropped for single
-method specifications without arguments.
+``\texttt{?}'' (try), ``\texttt{+}'' (at least once).  In practice, proof
+methods are usually just a comma separated list of
+\railqtoken{nameref}~\railnonterm{args} specifications.  Thus the syntax is
+similar to that of attributes, with plain parentheses instead of square
+brackets.  Note that parentheses may be dropped for single method
+specifications without arguments.
 
 \indexouternonterm{method}
 \begin{rail}
-  method: (nameref | '(' methods ')') (() | '?' | '*' | '+')
+  method: (nameref | '(' methods ')') (() | '?' | '+')
   ;
   methods: (nameref args | method) + (',' | '|')
   ;