diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 527226f687..89b8107ed7 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3836,13 +3836,15 @@ Abort. This command can be used to cut the proof-search tree according to a regular expression matching paths to be cut. The grammar for regular - expressions is the following: + expressions is the following. Beware, there is no operator precedence + during parsing, one can check with \texttt{Print HintDb} to verify the + current cut expression: \[\begin{array}{lcll} e & ::= & \ident & \text{ hint or instance identifier } \\ - & & \texttt{*} & \text{ any hint } \\ + & & \texttt{\_} & \text{ any hint } \\ & & e | e' & \text{ disjunction } \\ - & & e ; e' & \text{ sequence } \\ - & & ! e & \text{ Kleene star } \\ + & & e e' & \text{ sequence } \\ + & & e * & \text{ Kleene star } \\ & & \texttt{emp} & \text{ empty } \\ & & \texttt{eps} & \text{ epsilon } \\ & & \texttt{(} e \texttt{)} & |