Proof General is a generic front-end to several proof assistants such as Coq

The Proof General package provides a generic front-end to several proof assistants. It facilitates development by sending lines from a source file one by one to the proof assistant's read-eval-print loop and understands backtracking. It is actively maintained for Coq, and can also support Isabelle, HOL, ACL2, LEGO, Phox, as well as OCaml and Haskell to some extent.

External links