MML

MML has been under development since late 1988. By the time the CCL project started, MML already had 422 articles and covered, to varying levels of detail, several quite diverse areas (see [46]). MML is in essence developed by ``hobbyists'' in the sense that only sporadically there are sufficient funds available to organize larger teams for more focused efforts. In its initial years, CCL was one such case Over the years, the work on formalizing the CCL-book has been supported partially by grants from: ONR N00014-95-1-1336 and N00014-97-1-0777 (USA), KBN 8 T11C 018 12 (Poland), NSERC OGP 9207 (Canada), NATO CRG 951368, JSPS P00025 (Japan) and Shinshu Endowment Fund for Information Science (Nagano, Japan). .

Most of MML contained frequently used material covering the basic mathematical toolkit:

• operations on sets, relations and functions,
• ordinal and cardinal arithmetic,
• ordering and equivalence relations,
• natural, integer, real and complex numbers,
• finite sequences.

The following topics of interest for the formalization of the CCL-book were covered in MML to some degree:

• fundamental algebra: semigroups, monoids, groups, rings, fields, modules, and vector spaces;
• fundamental topology: basic definitions, metric spaces, and discrete spaces;
• posets and lattices, complete lattices, and numerous instances of lattices.

It was not at all clear to what degree this material could be used in its original form for the CCL project, see Section  for some numbers.