Hi Josef, >I remember making the Why Mizar environment work with newer >MML about a year ago (for Mikolas Janota >(http://www.ms.mff.cuni.cz/~janom9am/) experimenting with >Why). Did this just involve changing the "support article", or also involve patching the Why source code? It would be nice if the Why thing would keep working with newer versions of the MML automatically, don't you think? Freek