Minor reformat.

support for real valued preferences;

support for real valued configuration options;

support for floating-point tokens in outer syntax (coinciding with inner syntax version);

merged

added rule let_mono

CONTRIBUTORS;

more sharing of operations, without aliases;

simplified data lookup;

export declarations by default, to allow other ML packages by-pass concrete syntax; proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts); tuned;