tuned proofs;

tuned;

tuned;

tuned;

clarified signature;

proper pattern (amending 40a365360680);

more timing;

tuned;

tuned comments;

tuned;

prefer abstract command kind (in contrast to 367f4512e65c);

tuned;

tuned: avoid warning in IntelliJ IDEA;

more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL;

tuned signature;

clarified signature: do not require finished theory;

clarified modules;

merged

added lemmas multp_mono_strong and mult_mono_strong

merged

support for FoilTeX with demo document;

tuned comments;

tuned whitespace for "isabelle doc" display;

support for Easychair style with demo document;

support for Dagstuhl LIPIcs style with demo document;

clarified signature;

tuned signature;

tuned;

tuned signature;

clarified modules;

tuned;

tuned signature, following hints by IntelliJ IDEA;

restructured

modulus for polynomials is invariant wrt. units

proper Java syntax (amending ea79c21bcc47);

reactivate emerging tool after release (see 322f2e2799a7);

separate out definition of bound to avoid spurious sort hypotheses (by Jan van Brügge)

merged

Beautification of some declarations

merged

more robust etc/preferences: default value remains;

formal bundling for Admin/build_release: avoid confusion about presence or absence in manual invocations;

Beautifying CTT a tiny bit

A couple of new theorems. Also additional coercions to the complex numbers

more macOS platforms, without reference hardware;

official release;

merged

Added tag Isabelle2022 for changeset 1ac2416e8432

tuned signature (again, amending f32ac01aef5e), e.g. relevant for Isabelle/DOF;

tuned signature, e.g. for Isabelle/DOF;

updated to naproche-20221024: minor changes to documentation;

Replaced some ugly legacy proofs

more thorough cleanup;

tuned;

tuned: more robust Scala syntax;

merged

no compression for database server: let PostgreSQL/TOAST do the job;

prefer Zstd compression, notably for database exports;

tuned: avoid redundant copy of potentially large array;

merged

tuned proof

clarified signature; more direct Zstd compression using arrays instead of streams;

tuned signature, following isabelle.setup.Environment;

tuned signature;

tuned signature;

tuned signature;

clarified signature;

prefer new instance, following "make" signature terminology;

generic support for XZ and Zstd compression in Isabelle/Scala; support for Zstd compression in Isabelle/ML;

clarified signature: default cache is actually dummy and not changed dynamically;

clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;

support for Zstd data compression;

enforce fresh build;

merged

more robust read_file: prefer implicit replacement of bad input instead of failure via MalformedInputException;

more informative errors, with optional exception trace as in Command_Line.tool;

more robust reset of CLASSPATH: unset variable means "." in certain situations, e.g. scalac;

proper chapter for each ROOT file (amending b07f2ff55144);

tidying of ugly legacy proofs

Tidying of old and ugly proofs

deleted unused material

A bit of tidying

merged

Slight tidying of legacy proofs

merged

update naproche component;

Added tag Isabelle2022-RC4 for changeset 8b4108f41c77

rebuild with proper Isabelle version;

removed junk;

more robust, e.g. for "isabelle dump";

more robust, e.g. for "isabelle dump";

more robust, e.g. for "isabelle dump";

allow spaces in SCALA_HOME directory name;

avoid spurious error messages, e.g. when scala is missing;

more NEWS;

tuned, following hints by IntelliJ IDEA;

avoid result based on outdated state, e.g. relevant for use_theories with changed files;

tuned signature;

tuned signature, following hints by IntelliJ IDEA;

more robust treatment of state and events;

tuned signature;

proper result state (amending 954640e846d6);

tuned;

tuned signature;

tuned;

tuned signature;

tuned: clarified old_theory (in contrast to 4d5342898b1);

tuned signature;

more robust: active consumer for check_state/check_progress;

proper update of non-committed theories (see also 2bf1d0e57695, 2a1583baaaa0);

tuned;

tuned;

proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with symbols like \<^here>;

merged

added lemma fmember_iff_member_fset

tiny renaming

merged

Added the multiset termination proof

generate some metainformation not only for SPASS but also for Zipperposition, for experimentation

added lemma wfP_subset_mset[simp]

Tidying of some very old proofs

merged

tidying of some old proofs

merged

new contributor

more List lemmas (partly by Jeremy Sylvestre)

merged

merged

Trying to clean up some messy proofs

Mostly, removing the unfold method

Mostly trivial simplifications

Removal of the "unfold" method in favour of "unfolding"

Elimination of the archaic ASCII syntax

strengthened lemmas preorder.reflp_ge[simp] and preorder.reflp_le[simp]

added lemmas linorder.totalp_ge[simp], linorder.totalp_greater[simp], linorder.totalp_le[simp], and linorder.totalp_less[simp]

NEWS

merged

fixed NEWS following cee0b9fccf6f

renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with image_mono and to distinguish from inj_on_subset

merged

proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning "Nothing to build";

tuned whitespace;

less ambitious Bytes.chunk_size, which is presumably more stable with memory management under heavy load;

tuned comment;

support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes more stable than native ARM64;

updated to repository version polyml-test-bafe319bc3a6, which is presumably more stable (especially for ARM64);

more robust: prefer Windows $USERNAME;

proper home directory for ssh configuration (e.g. ~/.ssh/config); avoid redundant mkpasswd + mkgroup information, as recommended by Cygwin documentation;

more NEWS;

clarified signature: more arguments;

added lemma fimage_strict_mono

added lemma wfP_pfsubset

added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and wfP_if_convertible_to_nat

update components.sha1;

proper description;

one more lemma

merged

adjusted proofs

added and reorganized lemmas (some suggested by Jeremy Sylvestre)

removed redundant lemma

moved theorem from Fun to Set

added lemmas antisymp_ge[simp], antisymp_greater[simp], antisymp_le[simp], and antisymp_less[simp]

added lemmas reflp_ge[simp] and reflp_le[simp]

removed unused universal variable from lemma reflp_onI

added lemmas irreflD and irreflpD

added lemmas antisym_if_asym and antisymp_if_asymp

strengthened lemma total_on_singleton and added lemma totalp_on_singleton

generalized type classes as suggested by Jeremy Sylvestre

euclidean division on gaussian numbers

tuned proof

note on signed division on words

tuned definition

spelling

tuned proof

slightly less abusive proof pattern

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

Added tag Isabelle2022-RC3 for changeset d704efeb01db

proper cygwin component (see d042947e47a3)

proper base names;

suppress command echo in output;

include openssh for rsync (see also a1c7829ac2de);

provide naproche-20221002;

merged

clarified signature: more operations;

tuned signature;

tuned, following hints by IntelliJ IDEA;

clarified signature, to support external tools like "isabelle narration";

syntactic type classes for signed division operators

reduce prominence of facts

clarified signature;

more explanations on the new order prover (based on 10945fc183cd), without violating strict monotonicity of NEWS wrt. official releases;

restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;

added documentation about new order prover - new prover for partial and linear orders by Lukas Stevens and Tobias Nipkow - See NEWS for more context

tweaked

tweaked;

moved relevant theorems from theory Divides to theory Euclidean_Division

amend jenkins ci build;

restructured ci profile into modular ci build system;

more structured proofs

fixed some theory presentation issues (?)

recover informal "&" from 0c18df79b1c8;

added a couple of structured proofs

More obsolete "unfold" calls

getting rid of apply (unfold ...)

More syntactic cleanup. LaTeX markup working

more modernisation of syntax

Removal of obsolete ASCII syntax

clarified options;

merged

provide missing LaTeX macro, e.g. for AFP/PAC_Checker;

clarified signature;

streamlined division on polynomials

streamlined division on polynomials

clarified signature: re-use store/cache from build results;

tuned signature;

clarified signature: persistent Node.source / Snapshot.source;

more examples;

proper filter (amending fb4215da4919);

clarified conditions: no_build is ok for presentation if "all_current" holds; tuned;

tuned;

tuned signature;

clarified presentation_sessions: work with partial results;

tuned signature: removed unused operations;

tuned;

tuned comments;

streamlined division on polynomials

clarified packaging;

merged

Added tag Isabelle2022-RC2 for changeset 778152d51e97

show SSH options in PIDE GUI;

inplace update: proper Linux version;

provide naproche-20220917;

clarified NEWS;

proper platform directory x86_64-linux, to have it purged for other platforms; tuned README;

MLton component for x86_64-linux;

clarified Docker base image;

proper file headers;

tuned messages;

support for ISABELLE_MLTON_OPTIONS, notably for Ubuntu 22.04 with external mlton executable;

omit menu for unfinished tool;