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).