clarified: use existing Thm.dest_ctyp_fun (which is more strict);

prefer exception TYPE, e.g. when used within conversion;

tuned signature -- more ctyp operations;

clarified group of "main" library sessions;

tuned signature -- more ctyp operations;

merged

tuned signature: more operations;

backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is

tuned

more document structure

tuned

more abbrevs;

obsolete;

merged

updated documentation;

avoid Isabelle symbols in URL;

formal URLs;

tuned spacing;

modernized tags: default scope excludes proof;

report document tags as seen in the text (not the active tag of Thy_Output.present_thy);

support "tag" marker with scope;

tidying up messy proofs about group element order

merged

simpler and stronger proofs

tuned;

tuned;

merge plus tidied three proofs

merged

merged

type instantiations for poly_mapping as a real_normed_vector

visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);

tuned signature according to ML version;

strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");

added document antiquotation option "cartouche";

allow faster navigation of directory hierarchy (reverting 69465c3e3560);

more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;

prefer local options;

tuned signature; tuned message;

clarified order;

merged

prod/sum fixes

Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

tuned layout;

updated screenshots;

ignore odd warnings;

tuned whitespace;

merged;

updated for release;