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;

clarified syntax;

tuned;

more thorough clean_proof;

clarified modules;

avoid global syntax for MinProof (amending e31271559de8);

treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);

discontinued Proofterm.Promise (cf. 725438ceae7c);

clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;

tuned comments;

proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;

tuned comments -- proper sections;

support export_proofs, prune_proofs; tuned comments;

clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;

tuned;

clarified exception;

tuned;

more accurate type information;

unused (see also 42fbb6abed5a);

discontinued ASCII syntax;

global declaration of abstract syntax for proof terms, with qualified names; clarified modules;

tuned;

tuned;

more operations: support type classes within the logic;

clarified export of sort algebra: avoid logical operations in Isabelle/Scala;

more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);

more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;

More results about measure and integration theory

More analysis / measure theory material

merged

more new material about analysis

added forgotten declaration provided by Florian Haftmann

merged;

updated to jedit_build-20190717: support more brackets;

updated to isabelle_fonts-20190717;

redundant;

tuned;

added \<llangle>, \<rrangle>; discontinued special rendering for old {* *};

tuned doc isar-ref;

added \<bbar>;

added \<sqdot>;

fixed renaming issues

merged