more operations;

tuned;

tuned: more direct Name.context for bounds;

Got rid of another 250 apply-lines

merged

more proof tidying

more predictable proof id;

more conservative cache: retain concurrent value;

clarified thm_header command_pos vs. thm_pos;

clarified signature, following zterm.ML;

tuned whitespace;

merged

uniform export via ztyp/zterm/zproof;

clarified signature;

tuned;

more operations;

clarified scope of cache: avoid nested typ_cache;

clarified scope of cache: per theory body;

tuned module structure;

clarified signature: more operations;

merged

tuned

added nicer proof

better poller: don't start job when same version is already running;

clarified: more uniform;

merged

added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger

More streamlining

merged

Revised mixfix and streamlined proofs

clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);

tuned output, following Isabelle/Scala;

clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;

clarified signature, following Isabelle/Scala;

afford larger example (see also ccf9241af217);

more scalable operations;

tuned;

tuned (see also 4879d0021185);

tuned signature;

merged

clarified signature: afford explicit Scala data types;

tuned signature;

tuned signature (again);

clarified signature: more self-contained paint_chunk_list;

clarified signature: more arguments;

tuned;

clarified popup layer (not relevant yet);

clarified signature;

misc tuning and clarification;

tuned;

tuned signature;

tuned website;

proper parse (amending dd86d35375a7);

allow updating reports via build_manager_database tool, e.g. to generate hg logs/diffs;

clarified;

clarified;

log and display components with empty (unknown) revisions to indicate that they are present;

tuned log: omit previous changeset;

take care of facts in cartouches

Simplified a few proofs

tuned display;

NEWS and CONTRIBUTORS;

tuned HTML display of ANSI colors for better readability;

render hg diff and log (on separate page);

clarified;

store hg log in addition to diff;

clarified names;

tuned;

NEWS: totalisation of ln

merged

Better multiplication and division rules for ln and log

ignore error code for "isabelle worker" (in contrast to eff08c3f89fe): avoid confusing "failed to work" messages via Build_Cluster.start;

disable old tests;

added lemma image_mset_diff_if_inj

added lemma minus_add_mset_if_not_in_lhs[simp]

last-minute correction: no simprule for ln_minus

merged

Totalisation of ln and therefore log and powr

merged

The changes needed to reduce the need to snoop on edits to theory files

tuned messages: whitespace following usual Isabelle conventions;

merged

reactivate mini2 long after upgrade (see also a11c461a1a3a);

NEWS;

tuned signature: expose internal limits for testing or add-on implementations;

tuned;

tuned;

tuned;

tuned;

clarified signature;

prefer official UTF-8 decoding (in contrast to 2541de190d92): this is also more efficient (factor 10-20);

tuned;

unused (see also c2f176a38448);

more robust message header: prefer explicit props_length/props_chunks over odd YXML.embed_controls;

tuned signature: more operations;

tuned comments;

tuned whitespace;

use ansi colored diffs;

add diffs to build manager;

clarified: components vs. extra components;

compress reports;

clarified build report;

merged

enforce rebuild of Isabelle/ML;

clarified signature, following 43323d886ea3;

clarified signature: more direct operation;

clarified signature: more direct Bytes.raw and subsequent UTF-8 default decoding;

clarified signature;

tuned;

unused;

tuned;

clarified signature;

unused;

tuned signature;

simpler theorem

clarified: control verbosity;

enforce rebuild of Isabelle/ML;

more uniform Bytes.read_stream vs. File.read_stream;

clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;

more specialized operations;