diff options
| author |  Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-30 13:06:54 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-30 21:06:38 +0200 |
| commit | 461417d3ecced06f67f8fd535e4028174069b3cc (patch) | |
| tree | c373e07abc1bd5d6cb6e51603941ca2e7e2108b7 | |
| parent | c8a4896b54a89385b0a7a539be952c3dc3493821 (diff) | |
Update the section of supported PAs
| -rw-r--r-- | README.md | 17 |
1 files changed, 11 insertions, 6 deletions
@@ -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. |