explicit reference to code_dt

made lift_bnf more robust for abstract types with 'phantom' type variables

rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO"; uniform baseline for "linux" and "linux_arm";

proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);

proper bash syntax (amending 0631dfc0db07);

tuned proof: avoid z3;

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

tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;

merged

more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);

strengthened class parity

proper accessible paths for web server;

more informative message (amending b8a6b2ec85a2);

merged

more robust: do not affect "$ISABELLE_HOME_USER/contrib" on master node;

avoid excessive ML heap on this 16GB node;

more robust (amending c9774306a879);

proper ISABELLE_PLATFORM_FAMILY within Isabelle/Scala, in contrast to historic settings;

clarified symbolic host name;

allow remote_build on this host (server-arm), without conflicts of this "isabelle_self";

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;