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;
Bool = FOL +
types bool 0
arities bool :: term
consts tt,ff :: "bool"
end