more systematic treatment of profiling mode;

tuned message;

prefer less intrusive tracing message;

clarified documentation: tracing messages are not shown here;

add missing file;

more formal ML profiling messages;

clarified modules;

Lukas Steven's more general fold foctions for maps

More general fold function for maps

follow Phabricator update 2021 Week 23;

tuned;

more formal theory and session names; tuned whitespace;

proper NEWS after Isabelle2021;

updated descriptions;

allow system option short form NAME for NAME=true for type string, not just bool; support short system options "-o document" and "-o system_log";

tuned;

more robust within session "HOL";

merged

suppress theories from other sessions, unless explicitly specified via mirabelle_theories;

clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);

refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;

tuned;

more uniform schedule_theories, notably for "present" and "commit" phase after loading;

tuned;

moved more legacy to AFP

clarified modules;

clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);

tuned;

more thorough update of required files (amending 1529c3eb6bac);

clarified examples;

tuned proofs;

misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);

tuned --- reduced source complexity;

proper usage (amending f7ea394490f5);

merged, resolving minor conflict;

allow build session setup, e.g. for protocol handlers;

unused;

tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);

clarified signature;

removed pointless option (see 3d0952893db8);

tuned --- avoid redundant future tasks from already loaded theories;

no comment --- topological order appears to be fine since 04-Mar-2013;

more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7);

moved stride option from sledgehammer action to main mirabelle

merged

new lemmas mostly about paths

lexorders the locale way

more accurate export morphism enables proper instantiation by interpretation

merged

some new and/or varient results about images

nicer statement of Liouville_theorem

more lemmas

max word moved to Word_Lib in AFP

more robust syntax;

unused;

clarified document export names;

tuned signature;

tuned;

tuned;

avoid former verbose_latex, which has been renamed to verbose in 52030acb19ac;

compose Latex text as XML, output exported YXML in Isabelle/Scala;

more direct index_entry: no positions required -- text is eventually moved to .ind file;

clarified signature;

clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");

tuned message, e.g. for Pure bootstrap;

proper signature export (amending b50f8cc8c08e);

syslog option for "isabelle build";

further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea);

merged

NEWS;

clarified index, more like formal @{element_ref};

clarified treatment of type constructors;

misc tuning and clarification;

tuned signature;

clarified context;

more uniform document antiquotations for ML: consolidate former setup for manuals;

clarified names;

clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;

clarified modules;

clarified modules;

tuned;

clarified signature: avoid dispatch via name;

clarified, e.g. type variables;

tuned index;

more ambitious default for index "is like";

tuned;

support for index entries;

tuned;

tuned signature;

clarified modules;

clarified old document build;

unused;

prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee;

prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document;

unused;

proper Unix lines;

prefer explicit option document_bibliography (actually ignored by build script);

explicit option document_bibliography;

proper bibliography;

discontinued obsolete "isabelle latex";

more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX; clarified ISABELLE_MAKEINDEX options;

default document_build (lualatex);

more robust: allow \printindex within the document;

clarified bash scripts, with public interfaces for user-defined Document_Build.Engine;

tuned signature;

option document_preprocessor;

show symbols in Isabelle/ML instead of perl;

more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile;

tuned --- more robust;

discontinued somewhat pointless "fixbookmarks": default output works sufficiently well;

more uniform bibtex error, without using perl (see 4710dd5093a3);

proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);

tuned;

clarified command-line options;

obsolete (see 5a3a2a52648d);

redundant: copy produced from session document_files;

clarified treatment of Isabelle .sty files;

option document_logo;

proper options;

option document_build refers to build engine in Isabelle/Scala; pdflatex is back as legacy build engine, e.g. for published proceedings;

redundant: tmp_dir is purged anyway;

misc tuning and clarification;

clarified modules;

tuned --- clarified corner cases;

more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases;

clarified signature -- avoid odd warning about scala/bug#6675;

tuned;

tuned;

clarified signature;

proper syntax of Scala 3;

enforce syntax of Scala 3;

things need to be ugly

merged

sorted as an abbreviation

mere abbreviation for logical alias

avoid unexpected output+behaviour when CDPATH is set

recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04);

avoid perl;

tuned signature --- following hints by IntelliJ IDEA;

ignore session build timeout, notably in AFP;

check timeout_ignored as in ML, before applying timeout_scale;

merged

proper build of required session images vs. build with Mirabelle presentation;

reactive "sledgehammer";

reactive "sledgehammer_filter": statically correct, but untested (no proof_file);

clarified command-line;

clarified signature; supporess empty results;

clarified signature;

clarified log content;

reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;

tuned;

unused;

unused (see 8ffc607c345d);

clarified signature: provide access to previous state;

clarified signature (see Scala version);

tuned signature;

avoid duplicate loading of ML file;

strict_sorted now an abbreviation

explicit type class operations for type-specific implementations

obsolete

added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran

merged

generalized type

basic setup of Isabelle setup tool --- pure Java, no dependencies;

merged

guess package more directly;

merged

Just one lemma

proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;

clarified platforms;

merged

proper jEdit.props (amending ff716ecb0805);

update to gmp-6.2.1, with support for arm64-darwin;

clarified platforms;

clarified options: implicitly support both x86_64 and arm64;

tuned whitespace;

centralized more lemmas

avoid Fun.swap

guide is out of focus

proper build for fresh target directory (amending d9823224fcfe);

put more resources into jedit_build component;

more brackets (see f6b453449cc6);

more brackets;

proper settings variable, amending 6e85281177df;

merged

tuned proofs --- avoid z3, which is absent on arm64-linux;

proper condition: z3 could be absent, e.g. on arm64-linux;

build auxiliary jEdit component in Isabelle/Scala; clarified directory layout;

separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);

tuned message;

clarified signature;

tuned signature;