NEWS;

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

added Set.size;

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

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

tuned whitespace;

tuned comments;

tuned signature;

clarified signature;

tuned signature;

tuned output;

removed junk (amending 236e43c8bb5b);

tuned;

tuned output;

clarified signature: more general operation Bytes.read_slice;

tuned performance: much faster low-level operation;

clarified signature: more explicit types;

clarified signature: more explicit types;

clarified signature: more explicit types;

uodated map update syntax

Adjusted to changes in distribution.

More explicit type information in dictionary arguments.

tuned

tuned whitespace

more uniform approach towards satisfied applications

more uniform approach towards satisfied applications

tuned

tuned

Tuned semicolons.

added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element

reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.

refactored proofs

added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element

reversed import dependency between Relation and Finite_Set; and move theorems…

more operations;

clarified theory_sizeof1_data: count bytes, individually for each data entry;

clarified operations for ML object sizes;

merged

simplified a lot of messy proofs

merged