diff options
| author | filliatr | 2003-12-16 15:54:06 +0000 |
|---|---|---|
| committer | filliatr | 2003-12-16 15:54:06 +0000 |
| commit | 22a24e1cadd4e1206db195c9ef19ca3130eb1bc8 (patch) | |
| tree | b679e3a64f57c8738388d08cc6627cc7a518f23a /doc/Recursive-Definition.tex | |
| parent | d418004b79b5f95898eafa0b5376d5afc30cd699 (diff) | |
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/Recursive-Definition.tex')
| -rwxr-xr-x | doc/Recursive-Definition.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex index 6da37204fa..ba9423409e 100755 --- a/doc/Recursive-Definition.tex +++ b/doc/Recursive-Definition.tex @@ -87,10 +87,10 @@ Restore State Initial. \begin{coq_example} Theorem Ack : nat -> nat -> nat. Intro n; Elim n. -Intro m; Exact (S m). +Intro m; exact (S m). Intros p Ack_n m; Elim m. -Exact (Ack_n (S O)). -Intros q Ack_Sn_m; Exact (Ack_n Ack_Sn_m). +exact (Ack_n (S O)). +Intros q Ack_Sn_m; exact (Ack_n Ack_Sn_m). Save. \end{coq_example} One can check that the term {\tt Ack} ({\it eg} : the above |