recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);

prefer host that is less likely to be down;

tuned: more antiquotations, avoid re-certification;

Rearranged a couple of theorems

New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero

merged

tidied more apply proofs

build_manager: change colors;

build_manager: display more info;

add tables to web_app;

tuned and clarified;

build_manager: store submitting user;

build_manager: terminate processes if cancelling does not work;

build_manager: log message when job is cancelled;

branches of case expressions may need to be eta-expanded

tuned;

tuned: more antiquotations;

tuned;

tuned: more standard Isabelle/ML;

clarified signature: prefer local context;

tuned: more antiquotations;

tuned: more explicit dest_Const_name and dest_Const_type;

tuned signature: more operations;

tuned: more explicit dest_Type_name and dest_Type_args;

tuned;

tuned signature: more operations;

tuned: more antiquotations;

got rid of references to system-generated names

tuned names

tuned names

merged

Reversed my brain-dead stupid change to divide_left_mono and divide_left_mono_neg

merged

time_function T_map can now be generated automatically.

Further divide_mono fixes

Fix for simplified divide_mono theorem

Migration of new material mostly about exp, ln

More simplification of a nominal example

merged

More simplification of apply proofs

less ambitious parallelism: avoid exhaustion of memory (64GB total);

tuned names;

merged

Adjusting the precedences to reduce syntactic ambiguity

disable thy_cache for now (amending 0b8922e351a3): avoid crash of AFP/Ramsey-Infinite due to exception THEORY "Duplicate theory name";

A lot of new material from the Ramsey development, including a couple of new simprules.

A massive reduction of some truly horrible proofs

merged

More simplification of proofs. Trying to fix the syntax too

clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;

tuned;

clarified order of operations: no_thm_names first;

more operations;

tuned;

more operations;

more operations;

clarified signature: more robust operations;

merged

clarified modules (see also e063c0403650);

more operations;

tuned;

tuned: more direct Name.context for bounds;

Got rid of another 250 apply-lines

merged

more proof tidying

more predictable proof id;

more conservative cache: retain concurrent value;

clarified thm_header command_pos vs. thm_pos;

clarified signature, following zterm.ML;

tuned whitespace;

merged

uniform export via ztyp/zterm/zproof;

clarified signature;

tuned;

more operations;

clarified scope of cache: avoid nested typ_cache;

clarified scope of cache: per theory body;

tuned module structure;

clarified signature: more operations;

merged

tuned

added nicer proof

better poller: don't start job when same version is already running;

clarified: more uniform;

merged

added lemmas wfp_on_antimono_stronger and wf_on_antimono_stronger

More streamlining

merged

Revised mixfix and streamlined proofs

clarified Isabelle/Haskell type Term, following Isabelle/Scala (see 446b887e23c7);

tuned output, following Isabelle/Scala;

clarified data representation: prefer explicit OFCLASS constructor, following datatype zterm;

clarified signature, following Isabelle/Scala;

afford larger example (see also ccf9241af217);

more scalable operations;

tuned;