more robust message;

A few more new theorems taken from AFP entries

merged

define_time_function: avoid unused let's

common type class for trivial properties on div/mod

more robust (amending 1600fb749c54), to support the following corner case: schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))" apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>) oops

proper test options;

proper history_base for linux_arm;

updated to PostgreSQL 12 on Ubuntu 20.04; more accurate command-line;

routine build + test for linux_arm;

disable test on "augsburg1": machine will be dismantled;

add approximation factors in build schedule to estimate build times more conservatively;

merged

Type class patch suggested by Achim Brucker, plus tidied lemma

rearranged and reformulated abstract classes for bit structures and operations

Three new lemmas

tuned proof: avoid z3 to make it work on arm64-linux;

update to jdk-21.0.2; enforce rebuild of Isabelle/Scala + Isabelle/ML;

make build process state protected to avoid copying in subclasses (e.g. for database connections);

add build_sync tag to sync certain options (e.g., build_engine) across build processes;

clarified Mercurial version: presumably the last version that supports both python2 and python3;

more robust: avoid crash on non-Linux systems;

clarified webserver names;

proper Apache.php_name;

proper packages for mercurial_setup on Ubuntu 22.04: building from source provides hgweb modules, and also provides a defined version (6.1.1 is also provided by Ubuntu 22.04);

tuned source structure;

more robust systemd configuration;

more robust nginx configuration, notably for "certbot --nginx -d DOMAIN";

tuned whitespace in generated file;

tuned;