*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8517 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 1 deletions

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 4c8ae6940c..b0c248f654 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -423,20 +423,45 @@ Qed.
 
 Just use the \reflexivity tactic.
 
+\begin{coq_example}
+Goal forall x, 0+x = x.
+intros.
+reflexivity.
+Qed.
+\end{coq_example}
+
+
 \Question[symmetry]{My goal is an equality, how can I swap the left and right hand terms ?}
 
 Just use the \symmetry tactic.
+%\begin{coq_example}
+%Goal forall x y : nat, x=y -> y=x.
+%intros.
+%symmetry.
+%assumption.
+%Qed.
+%\end{coq_example}
+
 
 \Question[transitivity]{My goal is an equality, how can I prove it by transitivity ?}
 
 Just use the \transitivity tactic.
-
+\begin{coq_example}
+Goal forall x y z : nat, x=y -> y=z -> x=z.
+intros.
+transitivity y.
+assumption.
+assumption.
+Qed.
+\end{coq_example}
 
 
 \Question[autowith]{My goal is solvable by  some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?}
 
 Use a base of Hints.
 
+
+
 \Question[assumption]{My goal is one of the hypothesis, how can I prove it ?}
 
 Use the \assumption tactic.