1 files changed, 59 insertions, 0 deletions
diff --git a/README.md b/README.md
new file mode 100644
index 00000000..c508bcf1
--- /dev/null
+++ b/README.md
@@ -0,0 +1,59 @@
+# Proof General — Organize your proofs! 
+
+Proof General is a generic Emacs interface for proof assistants.
+The aim of the Proof General project is to provide a powerful, generic
+environment for using interactive proof assistants.
+
+This is version 4.4 of Proof General.
+
+## Setup
+
+Download and install Proof General from GitHub:
+
+```
+git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
+make -C ~/.emacs.d/lisp/PG
+```
+
+Then add the following to your .emacs:
+
+```
+;; Open .v files with Proof General's Coq mode
+(require 'proof-site "~/.emacs.d/lisp/PG/generic/proof-site")
+```
+
+## More info
+
+See
+    INSTALL	     for installation details.
+    COPYING	     for license details.
+    COMPATIBILITY    for version compatibility information.
+    REGISTER	     for registration information (please register).
+    FAQ, doc/	     for documentation of Proof General.
+
+    <prover>/README  for additional prover-specific notes
+
+Links:
+
+    Wiki:		  http://proofgeneral.inf.ed.ac.uk/wiki
+    Lists:		  http://proofgeneral.inf.ed.ac.uk/mailinglist
+
+Supported proof assistants:  Coq, Isabelle, LEGO, PhoX
+Experimental (less useful):  CCC,ACL2,HOL98,Hol-Light,Lambda-Clam,Shell,Twelf
+        Obsolete instances:  Demoisa,Lambda-Clam,Plastic
+
+A few example proofs are included in each prover subdirectory.  The
+"root2" proofs of the irrationality of the square root of 2 were
+proofs written for Freek Wiedijk's challenge in his comparison of
+different theorem provers, see http://www.cs.kun.nl/~freek/comparison/.  
+Those proof scripts are copyright by their named authors.  
+(NB: most of these have rusted)
+
+Check BUGS files for some static problems and issues.  Please report
+new bugs on the Trac site at http://proofgeneral.inf.ed.ac.uk/trac.
+
+For the latest news and downloads, visit Proof General on the web 
+at: http://proofgeneral.inf.ed.ac.uk
+
+David Aspinall <da+pg-feedback@inf.ed.ac.uk>
+October 2011.