clarified ternary tries

clarified test parameters;

more tests: Windows + AFP (see also 1fd5f96e1da3);

dropped references to theorems from transitional theory Divides.thy

Tidied some messy proofs

Updated some archaic proofs

tuned def: patter matching needs more beautification

removed lemma wellorder.wfP_less

merged

enforce rebuild of Isabelle/ML;

clarified signature;

Base64: proper support for large Bytes, with subtle change of types (Bytes instead of String);

tuned: prefer Bytes operations;

unused;

proper treatment of long message blocks;

clarified sizes;

more scalable stream read operations;

minor performance tuning;

tuned;

tuned module structure;

tuned names;

imitate internal policy of ByteArrayOutputStream: capacity is doubled after first push;

tuned whitespace;

unused;

Bytes.Builder is unsynchronized, like java.io.OutputBuffer;

notable performance tuning: avoid overhead of higher-order functions;

more efficient equals: avoid somewhat slow sha1_digest (see also 29b761e290c5, 306f273c91ec);

more scalable compression, using Bytes.Builder.Stream;

tuned: more uniform, less ambitious;

tuned;

minor performance tuning;

minor performance tuning; clarified signature;

minor performance tuning;

clarified signature;

tuned;

tuned;

clarified signature;

minor performance tuning;

support large byte arrays, using multiple "chunks"; support incremental builder; clarified "limit" (valid >= 0) vs. "hint" (valid > 0); clarified byte access: prefer unchecked acces and iterators internally;

clarified File.eq_content, following 306f273c91ec;

tuned;

clarified hash and equality: depend on sha1 digest to be collision-free;

clarified signature;

tuned source structure;

tuned signature;

minor performance tuning;

proper sha1_digest: need to include offset + length;

clarified signature: pro-forma support for Bytes with size: Long;

minor performance tuning;

clarified signature (again);

tuned;

clarified signature: discontinue somewhat misleading Bytes <: CharSequence;

minor performance tuning;

clarified signature: more accurate types;

clarified signature;

tuned messages;

clarified web server paths;

sort web app parameters in list;

proper available hosts;

tuned proof

tuned comments;

add build_manager_database tool to restore db from log files;

use build log in build manager to store meta-data persistently;

add build log format for managed builds;

improve build manager log (for build_log);

clarified;

proper web server address;

clarified names: more canonical;

clarified;

remove unused;

tuned;

fixed NEWS

merged

tuned signature: more exports;

clarified signature: prefer internal Thm_Name.T over external Facts.ref;

more robust / permissive;

clarified signature: more operations;

tuned;

clarified operations, following pretty_thm_name;

more accurate treatment of Thm_Name.T;

renamed lemmas

merged

renamed theorems

renamed theorems

add title;

use build_cluster in ci builds;

merged

tuned alias names in formulas

renamed theorems

add favicon to web app;

merged

clarified data representation: prefer explicit type Thm_Name;

more operations, following Isabelle/ML;

clarified signature: more explicit operations;

clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);

clarified operations, including exceptions;