Proof General for Debian ======================== Proof assistant support ----------------------- The Debian Proof General package supports only Coq. The upstream version contains by default also support for Isabelle/Hol (Isar), PhoX, HOL Light. These are excluded because - Isabelle is always distributed with its own customized version of Proof General; better not to interfere with that. - PhoX Proof General is completely broken, see Proof General ticket #434. - HOL Light is still in the development/testing state. The upstream version can be configured to also support Lego, the CASL Consistency Checker, a shell, HOL, ACL2, Twelf, Plastic and Lambda-CLAM. But all these are classified as obscure, incomplete or obsolete in the upstream sources. If you want to see support for one of these excluded proof assistants in the Debian package, please file a bug report against proofgeneral. Prooftree --------- This version of ProofGeneral contains support for Prooftree. When Coq is started it looks at the version number and enables the Prooftree functionality for Coq versions >= 8.4beta. Currently, Prooftree must be installed manually (see http://askra.de/software/prooftree/). Manuals ------- The Proof General User's manual is available in package proofgeneral-doc or online at the Proof General website (http://proofgeneral.inf.ed.ac.uk). The Proof General Adapting manual is only available at the Proof General website (or by downloading the sources). -- Hendrik Tews , Thu, 16 May 2013 09:46:03 +0200