Add citations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2607 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 1 deletions

diff --git a/contrib/jprover/README b/contrib/jprover/README
index 2dfb42827..fa08415f7 100644
--- a/contrib/jprover/README
+++ b/contrib/jprover/README
@@ -28,6 +28,16 @@ JProver is a theorem prover for first-order intuitionistic logic.
 It is originally implemented by Stephan Schmitt and then integrated into
 MetaPRL by Aleksey Nogin (see jall.ml). After this, Huang extracted the
 necessary ML-codes from MetaPRL and then integrated it into Coq.
+The MetaPRL URL is http://metaprl.org/. For more information on 
+integrating JProver into interactive proof assistants, please refer to
+
+   "Stephan Schmitt, Lori Lorigo, Christoph Kreitz, and Aleksey Nogin, 
+   Jprover: Integrating connection-based theorem proving into interactive 
+   proof assistants. In International Joint Conference on Automated 
+   Reasoning, volume 2083 of Lecture Notes in Artificial Intelligence, 
+   pages 421-426. Springer-Verlag, 2001" - 
+   http://www.cs.cornell.edu/nogin/papers/jprover.html
+ 
 
 Structure of this directory:
 This directory contains
@@ -55,7 +65,7 @@ MetaPRL directory. Some parts of this file are modified by Huang.
 4. <jterm.ml> and <opname.ml> are modified from the standard term module
 of MetaPRL in meta-prl/refiner/term_std.
 
-5. The Jp tactic currently cannot prove formula as
+5. The Jp tactic currently cannot prove formula such as
    ((x:nat) (P x)) -> (EX y:nat| (P y)), which requires extra constants
 in the domain when the left-All rule is applied.