More material for Analysis and Complex_Analysis

merged

actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

Fix OS.FileSys.fileSize for Windows using the same approach as modTime.

Fix OS.FileSys.modTime for Windows. The correct way is to use CreateFile to…

Fix OS.FileSys.setTime to work for directories on Windows. Also minor fix to…

merged

More new theorems from the number theory development

update some links;

more uniform mailing lists;

proper orientation for right-associative operations;

merged

tuned signature;

tuned signature;

clarified signature, using right-associative operation;

obsolete --- superseded by SHA1.Shasum operations;

tuned signature;

clarified signature;

tuned --- implicit split;

tuned whitespace;

prefer explicit shasum: more robust due to explicit file names, which often…

tuned signature;

more uniform use of SHA1.Shasum;

proper Shasum.digest, to emulate old form from build_history database;

prefer explicit shasum;

prefer explicit shasum;

proper symbolic dependencies, e.g. for Demo_FoilTeX;

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…

clarified signature selection: SortedSet[String], which fits better to stored…

tuned;

tuned signature;

clarified modules;

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

proper compiler root for arm64;

more robust dependencies for Pure;

Update names to match thesis.

clarified "isabelle build_polyml": download and build everything for current…

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

build only if required, view only after proper build: thus avoid pointless…

tuned message;

clarified modules;

maintain document_output meta data;

clarified modules;

more logging;

avoid redundant SelectionChanged events;

proper components base, following "isabelle components -I": downloaded…

proper symbolic handle on component resources (see Isabelle/3eb3de867786);

proper symbolic handle on component resources:

more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920…

More of Manuel's material, and some changes

clarified message: old-style log is usually empty;

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

clarified messages, notably for session "Intro";

more general program start message;

merged

isabelle update -u cite -l "";

clarified terminology of inlined "PROGRAM START" messages;

clarified GUI;

less ambitious parallelism: avoid exhaustion of memory (40GB total);

clarified GUI: omit pointless search buttons, as real output is shown as markup;

more uniform use of Symbol.output, even in situations where its Symbol.encode…

merged

More new material thanks to Manuel

merged

tuning

alternate AFP tests on lrzcloud2, to fit better into one day;

more realistic timeout, based on CPU time;

adapted to Isabelle/9a60c1759543;

more realistic timeout, based on CPU time;

merged

support document preparation from already loaded theories;

clarified GUIs: keep related buttons together;

clarified GUI events;

clarified GUI events: ensure fresh output when switching pages;

proper program name, e.g. for session "Intro";

clarified GUI events: reset everything on session context switch;

clarified GUI events;

clarified GUI: avoid odd jumping pages on "Cancel";

more accurate output: avoid output_body from last run;

more accurate output: avoid output_main from last run;

clarified guard: avoid spurious auto builds;

removed unused operation from 3f50b24909df;

more accurate Word.capitalize: do not touch name;

automatically build document when selected theories are finished;

removed obsolete parameter (see 7c23db6b857b);

clarified signature: prefer semantic status;

defer build until document nodes are ready;

more operations;

clarified Document_Editor.Session: more explicit types, more robust operations;

clarified operation (without change of signature!);

pointless

Lots more new material thanks to Manuel Eberl

fixed looping proofs