[isabelle-dev] Proof General 4.1pre

Makarius makarius at sketis.net
Thu Jan 13 15:39:32 CET 2011

There is now a development snapshot of Proof General 4.1pre, provided by 
David Aspinall:


It looks pretty stable to me.  There are only few remaining entries at 

Are there still users of PG 3.x with recent Isabelle snapshots or versions 
from the repository?

The question is if PG 4.1 converges sufficiently fast for Isabelle2011, 
and if we should switch to the PGIP update for floating point settings. 
This would mean to discontinue 4.0 and 3.x altogether.

If there is the slightest doubt we can also keep the odd treatment of 
pgreal values in Isabelle2011 -- PG 4.1 would work nonetheless, despite 
our abuse of the protocol.


More information about the isabelle-dev mailing list