From f47da94d66ae02f4f396214967042334cb43cbeb Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 6 Apr 2001 07:28:01 +0000
Subject: V7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8166 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Tutorial.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'doc/Tutorial.tex')

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
-- 
cgit v1.2.3