diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /doc/rt/Tutorial-cover.tex | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'doc/rt/Tutorial-cover.tex')
-rw-r--r-- | doc/rt/Tutorial-cover.tex | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex new file mode 100644 index 00000000..b747b812 --- /dev/null +++ b/doc/rt/Tutorial-cover.tex @@ -0,0 +1,48 @@ +\documentstyle[RRcover]{book} + % L'utilisation du style `french' force le résumé français à + % apparaître en premier. +\RRetitle{ +The Coq Proof Assistant \\ A Tutorial \\ Version 7.1 +\thanks{This research was partly supported by ESPRIT Basic Research +Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.} +} +\RRtitle{Coq \\ Une introduction \\ V7.1 } +\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring} +\RRtheme{2} +\RRprojet{{Coq +\\[15pt] +{INRIA Rocquencourt} +{\hskip -5.25pt} +~~{\bf ---}~~ + \def\thefootnote{\arabic{footnote}\hss} +{CNRS - ENS Lyon} +\footnote[1]{LIP URA 1398 du CNRS, +46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.} +{\hskip -14pt}}} + +%\RRNo{0123456789} +\RRNo{0204} +\RRdate{Ao\^ut 1997} + +\URRocq +\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la +v\'erification de preuves formelles dans une logique d'ordre +sup\'erieure incluant un riche langage de d\'efinitions de fonctions. +Ce document constitue une introduction pratique \`a l'utilisation de +la version V7.1 qui est distribu\'ee par ftp anonyme à l'adresse +\url{ftp://ftp.inria.fr/INRIA/coq/}} + +\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul +des Constructions Inductives} + +\RRabstract{Coq is a proof assistant based on a higher-order logic +allowing powerful definitions of functions. This document is a +tutorial for the version V7.1 of Coq. This version is available by +anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}} + +\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives +Constructions} + +\begin{document} +\makeRT +\end{document} |