tuned;

tuned signature;

tuned;

tuned signature;

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

tuned signature;

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

more robust: active consumer for check_state/check_progress;

tuned;

proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with…

tuned;

proof simplifications

merged

Simplified the proofs a bit

merged

replaced fmember.rep_eq by fmember_iff_member_fset

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…

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)

merge from afp-2021-1

only make parent dir;

accept all dois;

metadata toml: tuned error messages;

clarified sub topics;

merged

merged

Trying to clean up some messy proofs

Mostly, removing the unfold method

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

Mostly trivial simplifications

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.

NEWS

adapted to Isabelle/457f1cba78fb

fixed NEWS following cee0b9fccf6f

merged

renamed lemma inj_on_strict_subset to image_strict_mono for symmetry with…

merged

proper Deps.is_empty (amending 77327455b00d), e.g. relevant for warning…

tuned comment;

less ambitious Bytes.chunk_size, which is presumably more stable with memory…

tuned whitespace;

updated to repository version polyml-test-bafe319bc3a6, which is presumably…

support for system option ML_system_apple: emulated x86_64 Poly/ML is sometimes…

proper home directory for ssh configuration (e.g. ~/.ssh/config);

more robust: prefer Windows $USERNAME;

clarified signature: more arguments;

more NEWS;

added lemma fimage_strict_mono

added lemma wfP_pfsubset

added lemmas wf_if_convertible_to_wf, wfP_if_convertible_to_wfP, and…

update components.sha1;

proper description;

one more lemma

merged

extracted proof cases from lifting_lemma to distinct lemmas

added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;

tuned proof due to new simp rules

corresponding lemma was removed from distribution

merged

adjusted proofs

added and reorganized lemmas (some suggested by Jeremy Sylvestre)

moved theorem from Fun to Set

removed redundant lemma

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

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

updates to BenOr_Kozen_Reif by Katherine Kosaian

regen site

euclidean division on gaussian numbers

tuned proof

fix author entry; regen website

add change history revision

Added scene spaces, improvements to prisms, and improvements to the alphabet…

merge from afp-2021-1

new entry Query_Optimization

remove temp file

Complex_Bounded_Operators: Various changes:

slightly less abusive proof pattern

note on signed division on words

tuned definition

spelling

tuned proof

slightly less abusive proof pattern