Eclipse is an open source IDE originally developed by IBM. It started as a Java development environment, but has been re-engineered to be a general-purpose development environment. Plugins are available that provide state-of-the-art tools for working with a wide range of systems and projects. The Proof General Eclipse plugin supports theorem provers using the PGIP protocol.
Proof General Emacs is not yet as robust as PGEmacs but is now suitable for early adopters and small-scale use. Please help us by reporting problems and contributing improvements.