merged

Simplification of proofs

explicit range types in abstractions

somehow more clear terminology

tuned

Some basis results about trigonometric functions

merged

Even more new material from Eberl and Li

merged

More material for Analysis and Complex_Analysis

actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

merged

More new theorems from the number theory development

merged

proper orientation for right-associative operations;

tuned signature;

tuned signature;

tuned signature;

obsolete --- superseded by SHA1.Shasum operations;

clarified signature, using right-associative operation;

tuned whitespace;

tuned --- implicit split;

clarified signature;

prefer explicit shasum: more robust due to explicit file names, which often work implicitly in LaTeX;

tuned signature;

more uniform use of SHA1.Shasum;

proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types;

prefer explicit shasum; clarified signature;

proper symbolic dependencies, e.g. for Demo_FoilTeX;

prefer explicit shasum;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

clarified signature;

Some more new material and some tidying of existing proofs

more diagnostic operations (see also 5c7652e9bc01);

more thorough consolidation: follow dependencies of forked proofs (e.g. see theories MaxPrefix vs. MaxChop in AFP/Functional-Automata);

clarified signature selection: SortedSet[String], which fits better to stored json and works properly on Windows (NB: document theories have an authentic session-theory name);

tuned;

clarified modules;

tuned signature;

update to polyml-5e9c8155ea96, which is more robust on arm64;

more robust dependencies for Pure;

proper compiler root for arm64;

clarified "isabelle build_polyml": download and build everything for current platform; renamed former "isabelle build_polyml" to "isabelle make_poly", for experimentation and diagnosis;

no view_document after build: avoid loss of focus, especially in "auto build" mode;

tuned message;

build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;

clarified modules;

maintain document_output meta data;

clarified modules;

avoid redundant SelectionChanged events;

more logging;

proper symbolic handle on component resources: diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings 1c1,4 < classpath "$COMPONENT/lib/ci-extras.jar" --- > #-*- shell-script -*- :mode=shellscript: > > ISABELLE_CI_EXTRAS_JAR="$COMPONENT/lib/ci-extras.jar" > classpath "$ISABELLE_CI_EXTRAS_JAR" diff -r ci-extras-1/README ci-extras-2/README 11a12 > Makarius, 02-Feb-2023

more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);

More of Manuel's material, and some changes

less verbosity by default, notably for regular "isabelle build -o document";

clarified message: old-style log is usually empty;

clarified messages, notably for session "Intro";