HOW TO DEFINE TERMS IN MIZAR EFFECTIVELY
Selected contents from this journal
Languages of publication
This paper explains how proofs written in Mizar can evolve if some dedicated mechanisms for defining terms are used properly, and how to write articles to fully exploit the potential of these mechanisms. In particular, demonstrated examples show how automatic expansion of terms and terms identification allow to write compact, yet readable proofs.
Publication order reference
CEJSH db identifier