clarified background_foundation vs. theory_foundation (with const_declaration);

tuned;

more general standard_declaration; generic const declaration, which is applied to nested targets (named target only);

better restore after close_target;

tuned;

clarified standard_declaration vs. theory_declaration;

smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);

tuned;

tuned;

tuned signature;