diff options
Diffstat (limited to 'doc/refman/Omega.tex')
| -rw-r--r-- | doc/refman/Omega.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex index bbf17f630..b9e899ce8 100644 --- a/doc/refman/Omega.tex +++ b/doc/refman/Omega.tex @@ -16,7 +16,7 @@ may use any hypothesis of the current proof session to solve the goal. Multiplication is handled by {\tt omega} but only goals where at least one of the two multiplicands of products is a constant are -solvable. This is the restriction meaned by ``Presburger arithmetic''. +solvable. This is the restriction meant by ``Presburger arithmetic''. If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. |