diff options
| author | herbelin | 2003-03-13 13:16:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-13 13:16:53 +0000 |
| commit | 1682650f1c80774fac25bc41eaa15f4916917ecd (patch) | |
| tree | e53b268689933b812441e897b4925e08a056f2df /doc/Tutorial.tex | |
| parent | 7899f70633c86fbc404d4f96317c19a59395238e (diff) | |
Bug de pr�c�dence
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8329 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Tutorial.tex')
| -rwxr-xr-x | doc/Tutorial.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Tutorial.tex b/doc/Tutorial.tex index 7d408e57ae..60812f3538 100755 --- a/doc/Tutorial.tex +++ b/doc/Tutorial.tex @@ -544,7 +544,7 @@ naive user of \Coq~ may safely ignore these formal details. Let us exercise the \verb:Tauto: tactic on a more complex example: \begin{coq_example} -Lemma distr_and : A->(B/\C) -> (A->B /\ A->C). +Lemma distr_and : A->(B/\C) -> (A->B) /\ (A->C). Tauto. Save. \end{coq_example} |
