added lemma totalp_on_total_on_eq[pred_set_conv]

removed non-standard spaces in output

merged

avoid noise via context.progress (amending 68162e4f60a7);

more robust treatment of rsync on macOS (see also 96fb1f9a4042);

more robust: no change of directory attributes of initial test, notably target…

tuned whitespace;

merged

replaced HOL.implies by Pure.imp in reflp_mono for consistency with other lemmas

added lemmas reflp_on_Inf and reflp_on_Sup

added lemmas reflp_on_inf, reflp_on_sup, and reflp_on_mono

merged

clarified context with global defaults;

more robust: protect_args does not work with rsync 2.x from macOS, and is not…

clarified signature: more explicit type Rsync.Context;

tuned signature;

clarified signature;

clarified modules;

provide hugo-0.88.1 for darwin and linux;

provide python-3.10.4 for darwin and linux;

afp components: removed unnecessary platforms;

afp sitegen: switch to new version;

add sitegen ignore option;

improvements for toml module: proper boolean values;

add components as proper afp deps;

tuned;

more realistic timeout;

tuned whitespace;

removed obsolete self_update: always enabled, notably on lxbroy10 which is the…

clarified remote vs. local build_history: operate on hg_sync directory instead…

avoid redundant meta data: exclude .hg_archival.txt;

clarified signature: cwd can be misleading --- changes meaning of target;

proper operation on String, not Path;

more realistic timeout;

avoid hard-wired document;

more meta data;

merged

clarified signature: more operations;

tuned messages;

provide .hg_sync meta data;

clarified signature;

clarified options;

clarified signature (again);

more robust;

clarified signature;

NEWS

added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset

introduced predicate reflp_on and redefined reflp to be an abbreviation

removed usages of HOL.no_atp as its content and order is not guaranteed

switched to standalone cross-platform afp python component;

tuned;

afp python build: use tgz for better cross-plattform compatability;

replaced ci_profiles by statically compiled afp_build tool (Scala 3…

afp structure: added accessors;

hugo site: minor changes;

merged

hugo-site: improve various aspects;

add new authors to migration;

cleaning

insort renamings

merged

more operations;

support explicit SSH port;

redundant (after f28aee3ad1e6): self_update already takes care of currently…

clarified options;

Added lemmas

merged

Five slightly useful lemmas

clarified option -T;

preserve jars for quick testing;

clarified documentation: $ISABELLE_HOME is not a repository for regular…

tuned names;

clarified command-line options;

proper anchored pattern;

support thorough check of file content;

more documentation;

no separate code-equations required for a lift_definition by using (code_dt)…

clarified signature;

tuned messages;

tuned whitespace;

merged

support to synchronize Isabelle + AFP repositories;

support option -r;

more robust: local repository required;

tuned;

omit pointless option;

more documentation;

support for "isabelle hg_sync";

support filter rules, notably "protect";

clarified signature;

tuned comments;

clarified signature;

tuned signature;

tuned signature;

support rsync;

added lemmas Multiset.bex_{least,greatest}_element

added predicate totalp_on and abbreviation totalp

excluded dummy ATPs from Sledgehammer's default provers

move monotone from Complete_Partial_Order to Orderings

The last few occurrences of integrable_cong