support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);

removed junk;

merged

separated commands from annotations to be able to abstract about the latter only

prefer standard Term.dest_abs, with minor deviation of generated names;

tuned comments;

more examples

workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't;

more complete simp rules

more complete simp rules

avoid overaggressive contraction of conversions

normalizing NOT (numeral _) (again)

tuned text;

recover NEWS from 78d1f73bbeaa;

save 90 MB by excluding rlwrap and thus perl;

save 45 MB by excluding rlwrap and thus perl;

NEWS;

clarified test of directories;

misc tuning for release;

merged

updated to kodkodi-1.5.7. with more robust/portable management of files and processes;

provide minisat-2.2.1 on all currently supported platforms, notably as external solver for Nitpick;

tuned message;

proper build on macOS;

build minisat, using recent fork from original sources;

proper platform_path for executables run from Java;

tuned message;

tuned;

tuned whitespace;

merged

added timeout to veriT

new notion of infinite sums in HOL-Analysis, ordering on complex numbers

NEWS and CONTRIBUTORS

merged

added offset to Mirabelle's tptp output names

tuned zipperposition config in sledgehammer

considered slices overhead in sledgehammer

tuned atp_prover sliding

tuned Zipperposition slides in sledgehammer

include arm64-linux;

updated to Vampire 4.6, as proposed by Martin Desharnais;

build from official downloads;

build just one vampire version;

clarified signature;

maintain previous theory identifier to support semantic caching, notably in Isabelle/Naproche;

more exports, notably for Isabelle/Naproche;

include arm64-linux;

prefer existing OCaml installation;

include arm64-linux;

no patchelf on macOS (undetected due to cached executables?);

provide opam-2.1.0 for experimentation;

rebuild cygwin-20211004.tar.gz;

include arm64-linux;

updated to cygwin-20211004: build again;

merged

removed pointless NEWS: both Docker/ubuntu and Cygwin provide perl by default;

actually use cygwin-20211002 (amending ff0ca375457c);

discontinued perl;

clarified signature;

proper term operation Term.dest_abs;

tuned;

tuned proofs; fewer warnings;

more standard binder syntax;

clarified 'let' syntax: avoid conflict with existing 'let' in FOL;

tuned;

tuned;

merged

removal of a redundant theorem (and white space)

new material from the Roth development, mostly about finite sets, disjoint famillies and partitions

clarified and updated for release;

formal comment concerning 83d2208252d1 vs. d8dc8fdc46fc;

more NEWS and CONTRIBUTORS;

clarified comments;

support symbol \<Parallel>, based on \bigparallel from stdmaryd (stmary10.pfb: move y=1100, scale 222%, embolden by 40 units, adjust spacing);

clarified dependencies;

updated for release;

Added tag Isabelle2021-1-RC0 for changeset fedc0b659881

provide Isabelle/jEdit plugins as services, and thus allow user components do the same;

merged

updated for release;

misc tuning for release;

update dependency;

trim whitespace;

misc tuning for release;

misc tuning for release;

isabelle build_components -u;

updated to Haskell Stach lts-18.12 with GHC ghc-8.10.7;

updated to current Cygwin, near 3.2.0; discontinued perl;

updated to sumatra_pdf-3.3.3;

updated default version;

updated to xz-java-1.9;

updated to sqlite-jdbc-3.36.0.3;

updated to postgresql-42.2.24;

updated to jfreechart-1.5.3;

updated to flatlaf-1.6;

clarified signature;

clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;

clarified sledgehammer_provers, following d8dc8fdc46fc;

proper term operation Term.dest_abs;

tuned, following Syntax_Trans.variant_abs;

proper patterns for (- numeral t), amending 03ff4d1e6784;

tuned;

merged

update syntax for verit

clarified antiquotations;

clarified antiquotations;

provide verit-2021.06-rmx;

clarified antiquotations;

merged

clarified antiquotations; some comments concerning odd "- numeral";

clarified antiquotations;

clarified antiquotations;

merged

tuned TPTP parsing of THF function application

clarified examples;

repaired slip

merged

updated to Zipperposition 2.1

fixed veriT environment variable in sledgehammer's documentation

avoid overlapping PIDE markup (amending bb25ea271b15);