added support for unbounded max calls to Mirabelle

added warnings when defining unamed or redefining Mirabelle action

tuned whitespace;

tuned Mirabelle

merged

refactored Mirabelle to produce output in real time

Fix typo in date

more succint interfaces

global interpretation into nested targets

merged

tuned messages;

NEWS;

proper profiling within command execution: messages require PIDE id;

more systematic treatment of profiling mode;

tuned message;

prefer less intrusive tracing message;

add missing file;

clarified documentation: tracing messages are not shown here;

more formal ML profiling messages;

clarified modules;

Lukas Steven's changes for his fold updates

Lukas Steven's more general fold foctions for maps

More general fold function for maps

follow Phabricator update 2021 Week 23;

tuned;

more formal theory and session names;

proper NEWS after Isabelle2021;

updated descriptions;

tuned;

allow system option short form NAME for NAME=true for type string, not just…

more robust within session "HOL";

merged

clarified hook for Mirabelle: provide all loaded theories at once (for each…

suppress theories from other sessions, unless explicitly specified via…

refer to theory "segments" only, according to global Build.build_theories and…

tuned;

tuned;

more uniform schedule_theories, notably for "present" and "commit" phase after…

moved more legacy to AFP

moved more legacy to AFP

merge from afp-2021

merge from afp-2021

suppress site-gen warning

exclude etc/ in afp_check_roots

update usage instrucions

strip trailing whitespace; make full URL

sitegen for Lifting_the_Exponent

more robust component setup for AFP/thys: support "isabelle components -u" and…

new entry Lifting_the_Exponent

more specific export_files: omit recent additions ("document", "PIDE", etc.);

clarified modules;

clarified check (refining fc828f64da5b): etc/settings or etc/components is not…

tuned;

more thorough update of required files (amending 1529c3eb6bac);

clarified examples;

misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);

tuned proofs;

tuned --- reduced source complexity;

proper usage (amending f7ea394490f5);

allow build session setup, e.g. for protocol handlers;

merged, resolving minor conflict;

unused;

tuned --- potentially more robust (e.g. session.phase_changed vs.

clarified signature;

tuned --- avoid redundant future tasks from already loaded theories;

removed pointless option (see 3d0952893db8);

no comment --- topological order appears to be fine since 04-Mar-2013;

more predictable sequential presentation (2f9877db82a1), without somewhat…

moved stride option from sledgehammer action to main mirabelle

merged

new lemmas mostly about paths

grouped lemmas

lexorders the locale way

more accurate export morphism enables proper instantiation by interpretation

bundles for traditional infix syntax

some new and/or varient results about images

merged

nicer statement of Liouville_theorem

more lemmas

max word moved to Word_Lib in AFP

complement reduced to mere abbreviation

max word moved to Word_Lib in AFP

extracted more legacy abbreviations

merge from afp-2021

update website

fix links

Restore deleted theorem from Szpilrajn

tuned presentation

merge from afp-2021

adapted to devel

adjusted to changes in distribution

make AFP ROOTS globally available for component

merged

adjust Combinatorics_Words to isabelle@493b1ae188da

New entries Combinatorics_Words*

adjusted to change in distribution