From 461417d3ecced06f67f8fd535e4028174069b3cc Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 30 Aug 2018 13:06:54 +0200 Subject: Update the section of supported PAs --- README.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index 491f600a..bf6fdae5 100644 --- a/README.md +++ b/README.md @@ -115,12 +115,17 @@ Links: Supported proof assistants: -* 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 +* [Coq](https://coq.inria.fr/) +* [EasyCrypt](http://www.easycrypt.info/) +* [PhoX](http://www.lama.univ-savoie.fr/pagesmembres/raffalli/phox.html) + +Proof General used to support other proof assistants, but those +instances are no longer maintained nor available in the MELPA package: + +* Legacy support of + [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/) and + [LEGO](http://www.dcs.ed.ac.uk/home/lego) +* Experimental support of: 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. -- cgit v1.2.3