Update README.md.

- Specify the language for code excerpts
- Refactor the "More info" section.

1 files changed, 21 insertions, 22 deletions

diff --git a/README.md b/README.md
index e5e947e0..f14a8a65 100644
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@ This is version 4.4pre of Proof General.
 
 Remove old versions of Proof General, then download and install the new release from GitHub:
 
-```
+```sh
 git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
 cd ~/.emacs.d/lisp/PG
 make
@@ -18,41 +18,40 @@ make
 
 Then add the following to your `.emacs`:
 
-```
+```elisp
 ;; Open .v files with Proof General's Coq mode
 (load "~/.emacs.d/lisp/PG/generic/proof-site")
 ```
 
 If Proof General complains about a version mismatch, make sure that the shell's `emacs` is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On Mac in particular you'll probably need something like
 
-```
+```sh
 make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs
 ```
 
 ## More info
 
-See
+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
+* [INSTALL](INSTALL) for installation details
+* [COPYING](COPYING) for license details
+* [COMPATIBILITY](COMPATIBILITY) for version compatibility information
+* [FAQ](FAQ) for frequently asked questions
+* [coq/README](coq/README) for additional notes specific to the Coq prover
 
 Links:
 
-    Wiki:		  http://proofgeneral.inf.ed.ac.uk/wiki
-    Lists:		  http://proofgeneral.inf.ed.ac.uk/mailinglist
+* [https://proofgeneral.github.io/doc](https://proofgeneral.github.io/doc/) for online documentation of Proof General
+* [http://proofgeneral.inf.ed.ac.uk/mailinglist](http://proofgeneral.inf.ed.ac.uk/mailinglist) for mailing list information
+
+Supported proof assistants:
 
-* 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
+* Full support for latest versions of: [Coq](https://coq.inria.fr/)
+* Support for previous versions of:
+  [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/),
+  [LEGO](http://www.dcs.ed.ac.uk/home/lego),
+  [PhoX](http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html)
+* 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)
+A few example proofs are included in each prover subdirectory.