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;

more elementary swap

tuned comments;

misc updates and clarification;

clarified file name;

merged

updated to polyml-5.8.2 (official release);

clarified default_platform_families (again);

proper option for linux_arm;

proper "$?";

proper jvm_platform, notably for org.sqlite.lib.path;

tuned message;

support for platform family "linux_arm";

clarified purge;

removed junk;

support local build_heaps; more robust build_release;

merged

tuned --- rename = dist_name is sufficient;

proper dist_name;

clarified option -P: allow empty argument;

support for existing release archive; misc tuning and clarification;

tuned signature;

clarified signature;

more website content;

misc tuning and clarification: more explicit types Release_Context, Release_Archive;

tuned signature;

tuned theory structure

more appropriate location

collected lemmas on permutations