MMode A Mizar Mode for the proof assistant Coq. Abstract. We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics can be used with any interface of Coq, and they can be freely mixed with the normal Coq tactics.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element