more parallelism, at the cost of potential duplicates of make_thy;

afford more parallelism for sessions (instead of theories in 5eac4b13d1f1): depend on disjoint data areas (notably base.session_theories in 2ad892ac749a);

more interrupts;

present only selected session theories (as in Isabelle2021), in contrast to 2bc24136bdeb, eb89b3a37826; eliminated implicit state: these theories are globally unique;

tuned;

clarified modules;

tuned (see also e0d1d9203275);

clarified signature;

tuned;

spelling;

added asymp_{less,greater} to preorder and moved mult1_lessE out

renamed multp_code_iff and multeqp_code_iff

simplified mult_cancel_max and introduced orginal lemma as mult_cancel_max0

renamed Multiset.multp and Multiset.multeqp

added lemmas

merged

tuned;

removed redundant test (see also 86fac52c2795, a9fea3f11cc0);

just one Presentation.State for all sessions: avoid duplication of already presented theories (very slow) and cached theory export (not very slow);

proper version;

back to Z3 4.4.0pre for all platforms except arm64-linux: avoid failure e.g. in Padic_Ints (AFP/7a2522dce834);

less ambitious parallelism: more direct read/write saves overall heap space and GC time;

slightly faster XML output: avoid too much regrowing of StringBuilder;

updated NEWS: arm64-linux support is almost complete;

update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;

more material for HOL-Analysis.Infinite_Sum

more symbolic latex_output via XML;

clarified signature;

updated to polyml-5.9-610a153b941d -- close to final;

tuned signature (again): latex_output is likely to depend on context;

more symbolic latex output; discontinued Latex.output_text, which is in conflict with symbolic output;

tuned signature;

symbolic latex_output via XML, interpreted in Isabelle/Scala;

tuned signature;

clarified signature;

clarified signature;

clarified signature: more privacy;

tuned output --- less redundancy;

tuned whitespace;

clarified signature: Latex.Output as parameter to Document_Build.Engine; tuned;

proper detection of ARM platform variants;

back to post-release mode;

updated for release;

Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5

merged

updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default);

clarified HTML_Context: more explicit directory structure;

tuned comments;

tuned;

clarified signature;

clarified properties: avoid empty entry;

tuned signature;

merged

tuned (thanks to J. Villadsen)

added padding to Mirabelle's output

merged

tuned generation of TPTP with $ite/$let in higher-order logics

tuned generation of TPTP with $ite in function position

tuned TPTP generation of If helper facts

merged

clarified signature: prefer static operations;

clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;

more robust;

tuned signature;

clarified signature: more explicit class Entity_Context with private state + operations;

more hyperlinks, notably internal fact references;

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO

A tiny bit of tidying connected with Zorn's Lemma

tuned;

tuned;

proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);

revert temporary workaround 6d111935299c;

added lemma

merged

tuned attributes to avoid looping

added eq_iff_swap for creating symmetric variants of thms; applied it in List.

tuned text;

more robust timeout, following df4449c6eff1;

more accurate Files.isRegularFile, exclude directories (e.g. jar_path);

proper java_version for isabelle_setup;

explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;

tuned;

repackage minisat-2.2.1 with cygwin1.dll: required to run the executable without existing Cygwin context (normally provided by bash_process);

discontinued redundant document_preprocessor: in the worst case, a plain-old document/build script will do;

clarified messages, depending on option "document_echo";

just one cache, via HTML_Context, via Sessions.Store or Session;

merged

new lemmas about convex, concave functions, + tidying

proper support for arm64;

no perl (amending 59ef23ac81ab);

merged

Added tag Isabelle2021-1-RC2 for changeset b92b5a57521b

merged

Preserve variable name z in VAR {z = t}

back to scala-2.13.5: avoid crash of Scala REPL on arm64-darwin;

updated to polyml-5.9-5d4caa8f7148, which also contains ARM64 on darwin (unused by default);

more precise URL

tuned page breaks

cover all possible kinds, notably for references outside of this theory (amending 129fb11b357f);

proper foundational order;

back to non-strict Export_Theory.read_theory (without warning): theories could have been skipped due to "condition";

use all entity kinds from theory export, e.g. "method", "attribute";

clarified signature;

clarified physical_ref;

proper treatment of session build hierarchy;

proper used_theories for session build hierarchy, not known_theories from imported sessions;

present theories from imported sessions as required;

avoid multiple copies of fonts; proper fonts prefix for aux. files;

more compact persistent data;

tuned;

proper term_cache;

prefer "NAME|KIND" format, as already used in Isabelle/MMT and Isabelle/Dedukti;

tuned;

observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid;

tuned;

clarified order: prefer bottom-up construction of partial content;

more thorough update_global_index: overwrite old content;

tuned;

tuned;

clarified HTML_Context: just one context type;

unused (see also 217e6cf61453, 5e7916535860);

merged

clarified Theory_Cache: prefer immutable data with Synchronized variable; clarified Export_Theory.Theory vs. Entity tables; entity_ref: proper treatment of entity kind;

tuned signature;

unused;

proper support of verit's return code for timeout

tuned whitespace;

updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14";

clarified signature;

prefer official Export.explode_name; avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl;

tuned;

avoid conflict with future keyword;

tuned messages;

clarified signature: more direct XML.symbol_length;

more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it;

tuned -- eliminate clones stemming from d28a51dd9da6;

more to ANNOUNCE;

clarified link style: similar to Isabelle/jEdit;

tuned;

improved HTML presentation by Fabian Huch;

proper HTTPS;

proper markup type (amending be49c660ebbf);

merged;

more PIDE markup;

tuned signature;

more PIDE markup;

recover library_index_content.template from c337c798f64c: required for website/build/main;

merged

simplified some ugly proofs

more generous timeout: support build on Raspberry Pi;

add documentation for pred_mono

merged

added "mono" attribute to BNF generated pred_mono theorems

merged

do not declare $let-bound variables in TPTP output

IDE build actually works (but somewhat pointless);

suppress sources from jEdit/test, which prevent regular build of the generated scala_project;

removed junk;

improve pagebreaks by *not* using supertabular too much;

updated to scala-2.13.7 --- problems with jline disappear after purging $HOME/.inputrc;

more robust "isabelle scala_project": Gradle has been replaced by Maven;

tuned;

support linux_arm as well, e.g. native Docker on Apple Silicon;

update paths at TUM;

Added tag Isabelle2021-1-RC1 for changeset 81cc8f2ea9e7

updated for release;

some reordering for release;

updated to jdk-17.0.1+12;

tuned message;

clarified antiquotations;

tuned;

minor performance tuning;

more robust;

provide native executables for arm64-darwin, for more robust startup without Rosetta 2;

tuned proofs -- avoid z3, which is unavailable on arm64-linux;

prefer "sat_solver = MiniSat", to make examples work uniformly on all platforms;

discontinued pointless check of kodkodi_version, it is implicit in the bundled component;

tuned proofs -- avoid z3, which is unavailable on arm64-linux;

tuned;

test version of prespective polyml-5.9;

clarified antiquotations;

updated for pre-5.9 testing;

clarified antiquotations;

clarified antiquotations;

clarified antiquotations;

more robust subgoal addressing;

proper subgoal addressing;

clarified antiquotations;

recursive find_eq, not find_dist;

misc tuning and clarification;

clarified antiquotations;

order_tac: prevent potential bug, improve perf and tracing - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p.

misc tuning and clarification;

clarified antiquotations;

clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;

clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;

avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);

added Thm.instantiate_beta; tuned;

moved generic implementation into HOL-Main

tuned;

tuned;

clarified antiquotations;

clarified antiquotations;

discontinued somewhat pointless antiquotations;

NEWS;

clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;

clarified antiquotations;

clarified antiquotations;

clarified antiquotations;

clarified antiquotations;

support for "lemma"; support for "schematic" mode; clarified error position;

tuned;

local fixes for "lemma" antiquotation;

clarified signature;

tuned;

clarified keywords: major take precedence for commands, but not used for antiquotations; clarified modules;

tuned modules;

more antiquotations;

moved a theorem to a sensible place

merged

tuned, continuing e955964d89cb;

avoid waste of resources due to dynamic simpset (amending 45c09620f726);

fix latex

clarified modules;

more generic bit/word lemmas for distribution

merged

Added / moved some simple set-theoretic lemmas

more CONTRIBUTORS and NEWS;

cleanup; add Apple reference

refine interface

generalized component lookup for syntax and distinctness proofs. added some tracing.

merged

tuned;

more antiquotations;

more antiquotations;

more robust: genuinely free variables need to be instantiated;

tuned comments;

clarified errors;

tuned;

clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;