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;