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

a few new lemmas and a bit of tidying

support for a soft-type system within the Isabelle logical framework;

tuned

proper theory naming after join (reset due to merge_data);

support join of anonymous theory nodes, e.g. relevant for parallel theory construction;

clarified history stage: allow independent updates that are merged later;

support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);

proper quasi-total merge

made LaTeX happy

streamlined setup for linear algebra, particularly removed redundant rule declarations

tuned

tuned

even more appropriate fact name

more correct indicator

make latex happy

moved some theorems into HOL main corpus

misc tuning and modernization

more theorems for proof of concept for word type

official fact collection sign_simps

tuned proofs

avoid pseudo-collection to be used in generated proofs

moved comment to approproiate place

removed outcommented example which seems not to work as advertized

clear separation of types for bits (False / True) and Z2 (0 / 1)

generalized type classes for parity to cover word types also, which contain zero divisors

slightly more specialized name for type class