simplified make_option/dest_option;
added make_variant/dest_variant -- usual representation of datatypes;

explicit Document.Node.Header, with master_dir and thy_name;
imitate ML path operations more closely;

explicit indication of type Symbol.Symbol;

simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;

merged

added translation to fix critical pair between abbreviations for surj and ~=

floor and ceiling definitions are not code equations -- this enables trivial evaluation of floor and ceiling

merged

clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;

prefer Synchronized.var;