HOW TO DEFINE TERMS IN MIZAR EFFECTIVELY
Artur Korniłowicz · Studies in Logic Grammar and Rhetoric · 2009
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.