removal of ASCII connectives; some de-applying

tuned -- according to main website;

more ambitious compression;

tuned signature;

completion for \<^const>, although it often requires an extra argument;

proper treatment of root as directory;

tiny bit of extra restructuring

some variable renaming

tweaks esp renaming Rep_preal

Massive restructuring; deleting unused theorems

merged

partial updating to eliminate ASCII style and some applys

Added embedding_map_into_euclideanreal; reduced dependence on Equivalence_Lebesgue_Henstock_Integration in Analysis theories by moving a few lemmas

sequential build_release: it uses some of the test machines for pre-built images;

getting rid of most apply steps

consolidated map2 clones

separate type class for bit comprehension

no need to maintain two separate type classes

clarified structure of theories

follow convention of bold local syntax

more use of existing locales

avoid separate type class for mere definitional extension

tuned name

clarified notation

added lemma

incorporated various material from the AFP into the distribution

backed out experimental b67bab2b132c, which slipped in accidentally

merged

added lemmas

moved subset_image_inj into Hilbert_Choice

Lindelöf spaces and supporting material

hierarchically inclusive named theorem collections

removed unused fact collections

eliminated type class

entry point for comprehensive word library

tuned theory names

integrated Bit_Comparison into Word corpus

tuned

prefer one theory for misc material

moved instance to appropriate place

tuned for release;

clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);

afford more examples;

obsolete -- this is quite fast;

Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)

merged

markup fixes

merged

Towards a proof of algebraic closure (NB not finished)

tuned signature;

prefer ctyp operations;

meson: more cterm operations;

more ctyp operations;

tuned;

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