update Windows test machines;

More tidying of proofs

Another Nominal example

merged

Tidying up another Nominal example (SOS)

update Windows build host;

proper command-line;

Tidying up another of the nominal examples

More tidying of Nominal proofs

Tidied up another messy theory

More proof tidying for Nominal

Tidying up more messy proofs

Starting to tidy HOL-Nominal-Examples

sketch & explore: recover from duplicate fixed variables in Isar proofs

back to post-release mode -- after fork point;

merged

Added tag Isabelle2024-RC2 for changeset ef2134570abb

Acknowledgement of Ata Keskin for his Martingales material

merged

update to jdk-21.0.3; enforce rebuild of Isabelle/ML and Isabelle/Scala;

merged

Tidied up horrible archaic proofs

clarified signature;

make adhoc_overloading respect type constraints

merged

tuned;

clarified signature;

minor performance tuning: avoid redundant server access;

tuned;

clarified modules and options (from store);

clarified signature;

tuned;

clarified signature;

tuned signature;

tuned;

tuned signature;

tuned;

tuned;

more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);

tuned messages;

tuned;

back to static numa_nodes (reverting part of c2c59de57df9);

tuned messages;

canonical time function for List.nth

merged

Streamlining of many more archaic proofs

clarified web app parameters: more flexible, using HTML5 id specification (nonempty unicode string with no spaces);

More tidying of old proofs

merged

More tidying and removal of "apply"

Add subgoals variant of 'sketch' command

merged

Tidied some messy proofs

prefer canonical theorem name for fact collection declarations

merged

Tidying ugly proofs

tuned;

tweaked time functions for median-of-medians selection in HOL-Data_Structures

merged

rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;

Tiny tweaks to proofs

A bit of new material about type class "infinite", from Eval_FO

avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;

proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);

adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;

Add entry on Sketch_and_Explore to CONTRIBUTORS

moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory

more portable: prefer official JDBC operation DatabaseMetaData.getColumns();

tuned signature;

documented new syntax for fBall and fBex

updated for release;

Added tag Isabelle2024-RC1 for changeset 1231a7fb2510

misc tuning for release;

update for release;

merged

update to stack-2.15.5, stackage-lts-22.15;

clarified names: discontinue odd convention from 3 decades ago;

further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;

added documentation for meromorphicity etc. in HOL-Complex_Analysis

merged

merged

added special syntax for FSet.Ball and FSet.Bex

tuned proof

tuned proofs of Equiv_Relations.equiv

remove transitional (dummy) component list for Go

clarified signature: prefer authentic cterm used in Simplifier, avoid potential re-certification in user-code;

clarified names (see also 9c00a46d69d0, c5cd7a58cf2d); NB: Simplifier.set_trace_ops overrides Pure setup for Simplifier_Trace panel, but that is hardly every used in practice;

provide scala-3.4.1, but do not activate it: scala-3.3.x is LTS version;

clarified "bulky" sessions (again, see also 06153e2e0cdb), but note that "very_slow" is normally used together with "slow";

moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields

update NEWS;

moved web_app module from AFP (e.g., for building web services for the distributed build);

tuned;

removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML);

clarified signature;

clarified modules: more official Sessions.notable_groups;

tuned

merged

An assortment of new material, mostly due to Manuel

rebuild rsync-3.2.7 on current platforms, including native arm64-darwin; provide official etc/platforms.props, to retain platform directories after Components.Directory.clean() -- e.g. for SSH upload;

tuned signature;

tuned;

tuned signature;

merged

added lemma wfp_on_image and author name to theory

proper ISABELLE_GO_SETUP, e.g. for AFP/Go compiler tests;

proper "isabelle go_setup" for Jenkins;

dummy Admin/components/go to avoid crash of Jenkins (see 38bbc2ff3c24);

tuned message;

merged

tuned NEWS;

support for "all" platforms;

clarified signature;

merged

updated time functions for Array_Braun

merged

New material and a bit of refactoring

remove unused TEMP_WINDOWS more thoroughly (see also fa18208fd7bd and 37f852399a32);

tuned;

more robust Markdown;