diff options
Diffstat (limited to 'doc/Tutorial.tex')
| -rwxr-xr-x | doc/Tutorial.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex index f1d8123cbe..a525c5a213 100755 --- a/doc/Tutorial.tex +++ b/doc/Tutorial.tex @@ -976,9 +976,20 @@ symmetry of equality, for instance with tactics \verb:Transitivity: and \begin{coq_example} Apply foo. Transitivity (f O); Symmetry; Trivial. +\end{coq_example} +In case the equality $t=u$ generated by \verb:Replace: $u$ \verb:with: +$t$ is an assumption +(possibly modulo symmetry), it will be automatically proved and the +corresponding goal will not appear. For instance: +\begin{coq_example} +Restart. +Replace (f O) with O. +Rewrite f10; Rewrite foo; Trivial. Save. \end{coq_example} + + \subsection{Predicate calculus over Type} We just explained the basis of first-order reasoning in the universe |