more uniform treatment of properties (but < 0 should not occur here);

tuned signature;

clarified signature;

clarified signature;

misc tuning and clarification: more tight representation;

tuned: prefer "build" combinator;

tuned

tuned signature;

more operations for profiling;

provide rsync component, with uniform version + options on all platforms;

tuned message;

provide local component to remote directory;

tuned output;

more SSH operations;

more operations;

tuned comments;

clarified directory names, following bash_process (see e59d7d6fe1bd);

tuned README;

clarified build options;

more portable options;

build rsync from sources, to avoid divergence of protocols on various platforms;

more informative errors;

clarified options;

tuned messages;

provide Isabelle tool wrapper;

more robust errors: proceed updating database; clarified options; clarified progress;

tuned;

tuned output;

clarified signature;

clarified modules;

tuned comments (amending 1951f6470792);

tuned;

discontinue somewhat pointless is_single, which also depends on details of internal data representation;

more compact data: approx. 0.85 .. 1.10 of plain list size; fewer comparisons for Leaf2 / Leaf3: observe order;

slightly more compact data;

more operations, notably for profiling;

tuned;

more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;

tuned --- fewer compiler warnings;

tuned;

tuned;

tuned;

tuned signature: more uniform structure Key;

prefer Sortset.T for shyps;

tuned;

more operations;

tuned names: "e" means "entry" in table.ML and "elem" in set.ML;

NEWS;

added Set.size; tuned Set.merge: keep larger set stable;

performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;

performance tuning: prefer functor Set() over Table();

efficient representation of sets: more compact than Table.set;

tuned whitespace;

tuned comments;

tuned signature;

clarified signature;

tuned signature;

tuned output;

removed junk (amending 236e43c8bb5b);

tuned;