From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 doc/rt/Tutorial-cover.tex | 48 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 doc/rt/Tutorial-cover.tex

(limited to 'doc/rt/Tutorial-cover.tex')

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}
-- 
cgit v1.2.3