diff options
Diffstat (limited to 'doc/RefMan-int.tex')
| -rwxr-xr-x | doc/RefMan-int.tex | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/RefMan-int.tex b/doc/RefMan-int.tex index 649cfc3a9..1595dccf5 100755 --- a/doc/RefMan-int.tex +++ b/doc/RefMan-int.tex @@ -8,7 +8,11 @@ A new book~\cite{CoqArt} on practical uses of the \Coq{} system will be published in 2004 and is a good support for both the beginner and the advanced user. -The system \Coq\ is designed to write formal specifications, +%The system \Coq\ is designed to develop mathematical proofs. It can be +%used by mathematicians to develop mathematical theories and by +%computer scientists to write formal specifications, +The system \Coq\ is designed to develop mathematical proofs, and +especially to write formal specifications, programs and to verify that programs are correct with respect to their specification. It provides a specification language named \gallina. Terms of \gallina\ can represent programs as well as properties of these |