tuned imports;

add module for faster scheduled builds;

always use host database and make protected;

read relative cpu from build log;

prefer extensible next_node_info in build process over process_options in build engine (which needs the final node info anyway);

added start date to build jobs, e.g., for build time estimation;

added initial version of benchmark module, e.g., to compare performance of different hosts; added benchmark operation to build cluster;

generalized node infos: allow addressing of numa node segments via relative cpus; add more node options and process policy options using taskset as alternative to NUMA for more fine-grained cpu controls (e.g., for cpus with heterogeneous cores in the same NUMA segment);

add information about static host resources such as available NUMA nodes, cpus, etc. (e.g., for offline build planning);

added Range object to Host, e.g. to parse/unparse NUMA node ranges;

defined statically known tables of Build_Log; read hostname from build logs, store in Session_Entry (e.g., to track hosts in distributed build);

added lemma

added lemma

added lemma

NEWS and CONTRIBUTORS;

remove unused ci-extras component;

use mail module in CI build;

added mail module;

build javamail component and add to main components;

added component for javax mail;

updated to vampire-4.8;

tuned README;

update Vampire version, following hints by Martin Desharnais;

removed junk;

tuned component_vampire script for Vampire 4.8 and added new flag to force version name

prefer Isabelle options for CI mail settings over ci.properties;

Added the command nxsketch, which is like sketch except it separates these subgoals by "next" fills in the context using "fix"/"assume" rather than "for"/"if". Also the sketch command does the same if there is only one subgoal.

proper cut for Parse.enum1' and its derivatives (see also 769abc29bb8e);

unused (see fe9e590ae52f);

clarified modules;

merged

update documentation on simproc_setup;

tuned;

proper morphism;

simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe);

more compact ML source;

more robust read_simproc_spec: proper error positions;

tuned signature;

more standard simproc_setup using ML antiquotation;

more standard simproc_setup using ML antiquotation;

more standard simproc_setup using ML antiquotation;

added ML antiquotation "simproc_setup";

clarified signature;

clarified signature; clarified modules;

tuned signature;

tuned signature;

clarified signature;

clarified syntax and order of parameters;

clarified signature: Named_Target.setup works both for global and local theory;

clarified signature; clarified modules;

clarified signature: more concise simproc setup in ML;

clarified signature: more concise variations on implicit theory setup;

clarified simproc_setup (passive);

clarified 'simproc_setup';

support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);

more standard simproc_setup in Isar; recovered examples from dead comments;

more standard ML setup; proper tracing messages depending on context option, not Unsynchronized.ref; tuned whitespace;

proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0

added new portfolio for Vampire 4.8

tuned signature, following Isabelle/Scala;

more thorough expose_interrupt: always reset "break" state, regardless of pending interrupt;

tuned;

proper parallel build tasks;

more Haskell tests on macOS;

more NEWS;

disable naproche component for now: to be updated before the next Isabelle release;

updated to stack-2.13.1: include arm64-darwin, although it does not quite work yet (e.g. session "Haskell"); enforce rebuild of Isabelle/Pure and thus all Haskell applications;

more NEWS;

tuned structure;

update platforms: discontinue macOS 10.13 High Sierra, macOS 10.14 Mojave, macOS 10.15 Catalina;

updated to official release of polyml-5.9.1, based on Ubuntu 18.04 LTS and macOS 11 Big Sur;

proper options for macOS 11 Big Sur;

support for official release of polyml-5.9.1;

updated Linux baseline to Ubuntu 18.04;

support for macOS 14 Sonoma (only for testing);

more platform tests: initial support for macOS 14 Sonoma;

updated to gmp-6.3.0, for the sake of macOS 14 Sonoma;

merged

prefer Exn.result: avoid accidental capture of interrupts, similar to ML;

clarified user errors vs. failures, e.g. java.lang.StackOverflowError;

further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt;

proper Exn.capture with check_interrupt (amending a3dcae9a2ebe);

distinguish proper interrupts from Poly/ML RTS breakdown;

tuned;

tuned;

proper Isabelle_Thread.try_catch;

tuned;

proper Exn.capture / Isabelle_Thread.try_catch;

tuned;

clarified signature;

proper Exn.capture;

more robust: avoid race condition;

clarified name;

clarified signature;

clarified comments;

Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts

atin now an abbreviation for atin_within, which has been moved to Abstract_Limits

merged

New proofs also some slightly faster existing proofs

updated to hugo-0.119.0;

add component build tool for hugo from afp-devel;

removed test failing on some platform

mini2 is not active due to upgrade;

more PLATFORMS;

update documentation on Isabelle/ML exceptions;

misc tuning;

discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);

proper thread context for "isabelle-markup" Sidekick parser (amending 01a7265db76b);

proper Scala version, e.g. for IntelliJ IDEA;

NEWS

used standard Time.compare in Sledgehammer's preplay

moved variable bindings to tighter scope

removed proof reconstruction from Mirabelle; this is best handled directly in Sledgehammer

removed unused function parameter

merged

A couple of new lemmas

merged

more NEWS;

explicitly reject 'handle' with catch-all patterns;

avoid accidental 'handle' of interrupts;