diff options
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} |
