From 0e43e3479aa8865e2c26b7b977fd048c8195302f Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 23 Jun 2006 10:15:57 +0000 Subject: Mention de coqide, proof general et pcoq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/tutorial/Tutorial.tex | 29 +++++++++++++++++++---------- 1 file changed, 19 insertions(+), 10 deletions(-) (limited to 'doc/tutorial/Tutorial.tex') diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 4089d1c5f..4d6bbfa73 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -31,20 +31,29 @@ proof tools. For more advanced information, the reader could refer to the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y. Bertot and P. Castéran on practical uses of the \Coq{} system. -We assume here that the potential user has installed \Coq~ on his workstation, -that he calls \Coq~ from a standard teletype-like shell window, and that -he does not use any special interface. +Coq can be used from a standard teletype-like shell window but +preferably through the graphical user interface +CoqIde\footnote{Alternative graphical interfaces exist: Proof General +and Pcoq.}. + Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of \Coq, which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}. -In the following, all examples preceded by the prompting sequence -\verb:Coq < : represent user input, terminated by a period. The -following lines usually show \Coq's answer as it appears on the users -screen. The sequence of such examples is a valid \Coq~ session, unless -otherwise specified. This version of the tutorial has been prepared -on a PC workstation running Linux. -The standard invocation of \Coq\ delivers a message such as: +In the following, we assume that \Coq~ is called from a standard +teletype-like shell window. All examples preceded by the prompting +sequence \verb:Coq < : represent user input, terminated by a +period. + +The following lines usually show \Coq's answer as it appears on the +users screen. When used from a graphical user interface such as +CoqIde, the prompt is not displayed: user input is given in one window +and \Coq's answers are displayed in a different window. + +The sequence of such examples is a valid \Coq~ +session, unless otherwise specified. This version of the tutorial has +been prepared on a PC workstation running Linux. The standard +invocation of \Coq\ delivers a message such as: \begin{small} \begin{flushleft} -- cgit v1.2.3