Proof General for Debian ======================== Proof assistant support ----------------------- The Debian Proof General package supports only Coq and HOL Light. The upstream version contains by default also support for Isabelle/Hol (Isar), PhoX. 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. 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. Manuals ------- The Proof General User's manual is available in package proofgeneral-doc or online at the Proof General website (https://proofgeneral.github.io/). The Proof General Adapting manual is only available at the Proof General website (or by downloading the sources).