Piotr, >Does anyone have a better idea how to name issue that >Andrzej describes below In a sense it's about removing choices. That when you write a Mizar article there's only one "right" way to write it. But in a way I don't like that: because what if I don't like the "right" way, and want to write things the way that pleases me? Then the MML will work against me! Freek