forked from ProofGeneral/PG
-
Notifications
You must be signed in to change notification settings - Fork 0
This repo is the new home of Proof-General (http://proofgeneral.inf.ed.ac.uk/ will be updated soon)
License
ejgallego/PG
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
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.2 (prerelease) of Proof General. See About for exact version. It is built for Emacs 23.3. The code *may* also work with previous emacs versions, back as far as Emacs 22.3. But you will need to regenerated the byte-compiled files with "make clean; make compile". Backward compatibility cannot be guaranteed. 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: Bug/feature reports: http://proofgeneral.inf.ed.ac.uk/trac 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.
About
This repo is the new home of Proof-General (http://proofgeneral.inf.ed.ac.uk/ will be updated soon)
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- Emacs Lisp 79.0%
- Isabelle 7.8%
- OCaml 4.2%
- TeX 3.5%
- Coq 1.8%
- Makefile 1.2%
- Other 2.5%