On Tue, 9 May 2006, Freek Wiedijk wrote:
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?
just the support article
It would be nice if the Why thing would keep working with newer versions of the MML automatically, don't you think?
Yes. Question is how to maintain the articles automatically generated by various Why-like projects (if there are any pieces of mathematics worth maintaining in them). It can be either re-generated for newer MML each time, or included in MML and be revised together with MML. I guess these two methods will not always produce the same results. How is this done with the Coq library and the 4-color theorem, or HOL Light and Flyspeck?
Josef