Abstract This note describes Proof General, a tool for developing machine proofs with an
interactive proof assistant. Interaction is based around a proof script, which is the target of a
proof development. Proof General provides a powerful user-interface with relatively little
effort, alleviating the need for a proof assistant to provide its own GUI, and providing a
uniform appearance for diverse proof assistants. Proof General has a growing user base
and is currently used for several interactive proof systems, including Coq, LEGO, and …

This note describes Proof General, a tool for developing machine proofs with an interactive
proof assistant. Interaction is based around a proof script, which is the target of a proof
development. Proof General provides a powerful user-interface with relatively little effort,
alleviating the need for a proof assistant to provide its own GUI, and providing a uniform
appearance for diverse proof assistants. Proof General has a growing user base and is
currently used for several interactive proof systems, including Coq, LEGO, and Isabelle …