On Mon, 18 Sep 2006, Freek Wiedijk wrote:
Hi Piotr,I was under the impression the the Encyclopaedia of Mathematics in Mizar has been aiming, at least in part, at this goal.EMM will mean that you will know better where to look for lemmas. But you still will need to put things like XREAL_1 in multiple directives, which still is kind of silly. So it doesn't really help with making the environ sections substantially simpler.
I think both very strong refactoring (i.e. EMM - putting related things to one place) and simplified directives are useful. To compare e.g. with HOL Light, saying there
"needs "Multivariate/misc.ml;;"probably means that all stuff from misc.ml is imported, and recursively all its "needs".
So why not chase e.g. for general topology all the relevant stuff scattered over MML to just a couple of topological articles (that might also mean putting all the highly special "rubbish" to other place, where it will be silently forgotten), and then have something like
"needs topology" (or whatever) as a shortcut for including (recursively) all of them?It seems to me that once an article is submitted to MML (and published in FM, and all the glory belonging to the author properly recorded), it really should be "dismantled" into pieces which are put into proper parts of the MML structure. At least to the extent, that if someone submits a new topological article, the important stuff from it is accessible again when I write "needs topology".
Josef