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;

clarified modules;

recover Url.is_wellformed from before d8330439823a, e.g. relevant for JEdit_Resources.read_file_content (the URI alone does not necessarily have a protocol prefix, so plain file-path would be treated as URL);

proper php-fpm configuration for nginx;

support multiple webservers: Apache or Nginx;

tuned;

clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);

unused;

enforce rebuild of Isabelle/Scala + Isabelle/ML;

updated to postgresql-42.7.1;

updated to sqlite-jdbc-3.45.0.0, including slf4j-1.7.36;

update to llncs-2.23; update src/Doc/Demo_LLNCS to include the new mandatory section "Disclosure of Interests";

clarified bootstrap;

clarified directories;

clarified directories;

obsolete (see also fc88b943e1b2);

proper output, following 2cd23d587db9;

always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);

clarified directories;

more accurate Isabelle versions;

more accurate Ubuntu versions;

more uses of define_time_fun

translation to time functions now with canonical let.

merged

A few new results (mostly brought in from other developments)

merged

Added time function automation

streamlined type class specification

consolidated lemma name

support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";

merged

tuned;

update links;

follow post-maintenance updates of original Phabricator, as base-line for Phorge;

refer to "localhost" as pro-forma domain;

simplified specification of type class

consolidated name of lemma analogously to nat/int/word_bit_induct

more accurate syntax: 'obtain' vars are optional;

clarified order, disregard structure of proof;

minor performance tuning;

tuned;

more thorough treatment of hidden type variables within zproof;

more uniform treatment of "hyps" within zproof;

clarified order: follow Thm.fold_terms;

merged

clarified signature;

clarified signature;

tuned signature;

tuned;

clarified test: no exception yet;

tuned;

tuned;

tuned signature: more direct operations;

clarified signature;

clarified signature: more direct operations;

tuned signature;

tuned;

minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);

tuned whitespace;

more robust: certify types uniformly (see also 62b75508eb66);

tuned;

clarified signature;

clarified signature: avoid redundant Term.maxidx_of_term;

proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);

misc tuning and clarification: prefer Same.operation;

clarified signature;

tuned names;

clarified signature;

tuned whitespace;

clarified modules; minor performance tuning;

clarified signature;

added and removed lemmas

proper SMTP session: set envelope sender address correctly;

update javamail component with current jakarta mail APIs and eclipse angus implementation;

tuned source structure;

clarified signature; minor performance tuning;

tuned;

minor performance tuning; eliminate clones;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

tuned;

tuned signature;

tuned signature;

more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;

omit syntactic of_class check, which is in conflict with sort constraints within the logic;

tuned;

minor performance tuning;

clarified signature; clarified modules;

misc tuning and clarification;

tuned signature;

tuned signature: canonical argument order;

tuned;

clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);

clarified box_proof: use sort constraints within the logic;

more operations (see also 8368160d3c65);

proper support for complex types, not just type variables (amending 623789141e39);

proper instantiation for make_const_proof, notably change of types for term variables;

tuned names;

more operations;

clarified signature;

minor performance tuning: proper Same.operation;

minor performance tuning: proper Same.operation; clarified modules;

tuned signature;

minor performance tuning: proper Same.operation; clarified modules;

minor performance tuning: proper Same.operation;

tuned signature;

tuned;

pro-forma support for ZTerm.sorts_zproof;

tuned comments;

tuned structure;

minor performance tuning: proper Same.operation;

tuned names (again);

clarified modules;

clarified signature: more operations;

tuned names;

clarified signature;

tuned;

tuned whitespace;

clarified signature;

tuned;

tuned;

clarified signature: prefer Same.operation;

tuned;

more zproofs;

more operations;

clarified modules; minor performance tuning;

minor performance tuning, following 703201dbd413;

tuned;

clarified signature: suppress unused fields;

eliminate clone (amending e7796c55d840);

minor performance tuning;

more operations;

more operations;

tuned;

clarified store_proof: before attributes are applied, to ensure proper thm_proof boxes for declaration attributes;

tuned;

tuned signature;

tuned; more uniform Thm.transfer;

tuned;

more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;

clarified modules;

clarified signature;

tuned;

clarified Global_Theory.store_proofs vs. Generic_Target.thm_definition / Attrib.global_notes;

clarified signature;

tuned;

tuned: avoid duplicates;

more operations;

proper Thm.transfer;

proper Thm.trim_context;

clarified stored data: actual thm allows to replay zproofs in a modular manner;

tuned signature;

tuned signature, following Proofterm.thm_header;

more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;

clarified signature;

proper Thm_Name.make_list for thm_definition; tuned modules;

more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);

more robust: zproofs need to be enabled (amending 43d8385db923);

more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;

tuned names;

clarified signature: support update of local_theory;

tuned;

clarified modules;

tuned;

unused;

clarified modules;

tuned;

clarified modules;

tuned;

tuned signature;

tuned;

more operations;

eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);

minor performance tuning: shorter names;

minor performance tuning: static vs. dynamic rules;

minor performance tuning;

clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;

clarified signature;

tuned;

more thorough treatment of zproof vs. proof: avoid accidental storage of large structures;

clarified signature;

observe option "prune_proofs";

clarified zproof storage: per-theory table in anticipation of session exports;

proper thm_name for stored zproof;

uniform treatment of lazy facts: actual proof terms are always strict;

tuned;

tuned whitespace;

tuned;

proper Thm.transfer;

clarified context: avoid capture of thy2 within closure;

tuned names;

more informative exceptions;

more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");

tuned;

more informative exception;

clarified signature;

clarified ML toplevel output: avoid "??." prefix;

tuned;

merged

use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;

clarified signature;

omit pointless future: proof terms are built sequentially;

omit unclear / inaccurate renaming;

more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;

more robust: avoid assumption about Context.certificate_theory;

tuned;

clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);

tuned;

tuned;

more normalization;

less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);

tuned;