[isabelle-dev] NEWS: Proof General is now an optional component
makarius at sketis.net
Mon Jun 30 12:18:10 CEST 2014
* Proof General with its traditional helper scripts is now an optional
Isabelle component, e.g. ProofGeneral-4.2-2 from the Isabelle
component repository http://isabelle.in.tum.de/components/. See also
the "system" manual for general explanations about add-on components,
notably those that are not bundled with the normal release.
This refers to Isabelle/577f029fde39.
Remaining users of Proof General should have no problems to init such an
optional component, if not already done by default, based on
If the change breaks anything by accident, it should be reported here. I
do very little Proof General testing these days.
Note that the "true" way to use Proof General is by manual tinkering with
its elisp setup, based on the official distributiom from
http://proofgeneral.inf.ed.ac.uk/. David Aspinall was never quite happy
with my way of assimilating it into the Isabelle distribution many years
More information about the isabelle-dev