more qualified names -- eliminated hide_const (open);

tuned;

merged

local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;

support for 'restricted' modifier: only qualified accesses outside the local scope;

tuned;

clarified rail syntax;

@{command_spec} is superseded by @{command_keyword};

clarified command keyword markup;

more position information and PIDE markup for command keywords;

allow prefix before keyword, notably 'private';

support local command setup;

proper header; misc tuning;

tuned signature;

tuned;