[isabelle-dev] NEWS: Proof General is now an optional component

Makarius 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 mailing list