diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 08:54:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 08:54:24 +0000 |
| commit | 228c9739a6e94f52a1fd4d6439ee34af1f7a987a (patch) | |
| tree | 89d35da48600499ebe3d22a20b71b8781dfeb925 | |
| parent | 2ac2d20feadc39826a811fa3101f04836992889c (diff) | |
Aspect mathematique de Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8448 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |