diff options
| -rwxr-xr-x | doc/RefMan-pro.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index a65cd816e..79e0c8263 100755 --- a/doc/RefMan-pro.tex +++ b/doc/RefMan-pro.tex @@ -24,7 +24,7 @@ hypotheses we call the {\em \index*{local context}} of the goal. Initially, the local context is empty. It is enriched by the use of certain tactics (see mainly section \ref{Intro}). -When a proof is achieved the message {\tt Subtree proved!} is +When a proof is achieved the message {\tt Proof completed} is displayed. One can then store this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of $\lambda$-calculus, known as the {\em Curry-Howard |