From 6b5c2e6a810cf5852d670b7caf2f26e2e4e7a713 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Dec 2003 18:57:47 +0000
Subject: Ajout Admitted

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8438 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-pro.tex | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 3adecde1d5..b84d1b38a7 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -95,6 +95,10 @@ if the original goal has been opened using the {\tt Goal} command.
   Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
+\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted}
+This command is available in interactive editing proof mode to give up
+the current proof and declare the initial goal as an axiom.
+
 \subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem}
 This command switches to interactive editing proof mode and declares
 {\ident} as being the name of the original goal {\form}. When declared
-- 
cgit v1.2.3