record sort constraints unconditionally: minimal performance implications;

more careful export of unnamed proof boxes: avoid duplicates via memoing;

tuned signature;

export each PThm node separately: slightly more scalable;

allow duplicate exports via strict = false;

tuned message;

more positions;

more positions;

tuned;

formal position for PThm nodes;

clarified ML types;

proper treatment of body oracles, outside of recursion into thms graph;

prefer named lemmas -- more compact proofterms;

prefer named lemmas -- more compact proofterms;

tuned whitespace -- slightly more readable;

clarified signature: fewer warnings in ML IDE;

tuned;

prefer named lemmas -- more compact proofterms;

more compact proofterms;

eliminated pointless comments;

clarified proofterms;

more robust and convenient treatment of implicit context;

removed junk (cf. fa933b98d64d);

explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;

more careful treatment of implicit context;

more careful treatment of implicit context;

proper build options;

merged

backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;

more careful treatment of implicit context;

clarified signature; more careful treatment of implicit context;

more robust and convenient treatment of implicit context;

clarified context: proper transfer;

tuned;

clarified modules: more direct data implementation;

Added Takeuchi function to HOL-ex

full AFP test on lrzcloud2;

obsolete;

more efficient data structure;

clarified signature;

guard constraints by record_proofs=1, until performance implications have become more clear;

more complete completions according to Sorts.insert_complete_ars (cf. 13199740ced6), e.g. relevant for theories HOL-ex.Word_Type, HOL-Matrix_LP.SparseMatrix;

tuned;

tuned;

maintain sort constraints from type instantiations, with pro-forma derivation to collect oracles/thms; tuned;

more direct proofs for type classes; misc tuning and cleanup;

tuned;

clarified modules: inference kernel maintains sort algebra within the logic;

more elementary treatment of standard_vars (unconstrainT is already standard);

clarified module structure;

simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

abstract type theory_id -- ensure non-equality type independently of implementation;

clarified export: retain proof boxes as local definitions -- more scalable;

reduced dependencies

clarified global theory context;

more robust export, based on reconstruct_proof / expand_proof;

clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;

tuned -- fewer warnings;

discontinued pointless messages;

clarified context;

clarified modules;

discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;

merged

more diagnostic operations;

tuned -- non-strict args;

proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);

tuned signature;

clarified signature; tuned;

tuned signature;

News for bind infixl

Monadic bind is now infixl as is the norm

purge remains from test (cf. 5a53724fe247);

tuned;

clarified signature;

removed obsolete RC tags;

tuned;

clarified signature;

tuned;

tuned;

clarified signature;

tuned;

tuned;

tuned;

tuned -- reorder sections;

tuned;

proper argument type (amending 42fbb6abed5a);

tuned signature;

tuned;

finalize proofs earlier to reduce memory requirement;

proper proof_serial;

more explicit type proof_serial;

defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification;

more accurate proof definitions (PThm nodes);

avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");

prefer local counter;

more accurate proof export;