clarified signature: full dependency graph;

merged

more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;

tuned signature;

merged

simplified proofs

more rules for ordered real vector spaces

simplified setup

tuned proof

merged

enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;

support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

more scalable -- less ML heap requirements;

tuned whitespace;

Integrate locale activation fallback diagnostics with 'trace_locales'.

entry point for analysis without integration theory

removed Brouwer_Fixpoint from imports of Derivative

removed unused lemma, generalized, reduced dependencies

fixed typo

moved lemmas; reduced dependencies of Lipschitz

explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space

merged

moved lemmas

moved basic theorem

proper positions for 'termination' command (see also 5549e686d6ac);

tuned names -- proper scopes;

added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);

proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;

Tracing of locale activation.

tuned

always export Pure proofs;

clarified 'thm_deps' command;

more compact: avoid pointless PThm rudiments;

clarified signature: prefer total operations;

proper graph traversal: avoid multiple visit of unnamed nodes;

more scalable: avoid huge intermediate XML elems;

more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;

NEWS;

merged

export thm_deps;

proper theory context;

clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;

clarified signature;

tuned;

unused (see 095dadc62bb5);

tuned;

tuned signature;

clarified modules;

clarified modules;

tuned;

clarified signature;

tuned

tuned

merged

tuned

merged

clarified signature;

clarified export of axioms and theorems (identified derivations instead of projected facts);

tuned signature;

back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;

module Thm_Name for Isabelle/Scala;

tuned;

clarified modules;

tuned;

tuned

tuned names

clarified signature;

discontinued peek_status: unused and not clearly defined;

more documentation on oracles;

proper theory context for global props;

more thorough check, using full dependency graph of finished proofs;

added ML antiquotation @{oracle_name};

more robust, notably for open_proof of unnamed derivation;

tuned comments;

NEWS;

more accurate proposition for cheat_tac (command 'sorry');

added command 'thm_oracles';

clarified type for recorded oracles;

unused;

clarified signature;

clarified modules;

clarified lookup operations: more scalable for multiple retrieval;

clarified signature;

merged

maintain thm_name vs. derivation_id for global facts;

clarified identity of PThm nodes: do not reuse old id after renaming -- enforce uniqueness of substructures;

clarified signature;

Fixed brace matching (plus some whitespace cleanup)

merged

new material on eqiintegrable functions, etc.

clarified treatment of individual theorems; tuned messages;

tuned signature;

clarified signature;

clarified derivation_name vs. raw_derivation_name;

merged

more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;

more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;

support Export_Theory.read_proof, based on theory_name and serial;

clarified PThm: theory_name simplifies retrieval from exports;

Indexname.toString according to string_of_vname' in ML;

clarified type Indexname, with plain value Int; eliminated pointless cache_int;

more complete pattern match;

export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;

support for (fully reconstructed) proof terms in Scala; proper cache_typs;

new material; rotated premises of Lim_transform_eventually

clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);

tuned;

uniform standard_vars for terms and proof terms;

treat simproc results as atomic -- more compact proof terms;

tuned;

minor performance tuning;

NEWS and example for Theory.join_theory;

tuned whitespace;

more compact proof terms;

more documentation;

added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;

clarified modules;

merged

more compact proof terms;

more robust -- notably for metis, which tends to accumulate tpairs;

tuned -- avoid shadowing of ML names;

tuned;

more compact proof terms;

tuned;

tuned;

tuned -- eliminated unused parameters;

more direct/compact export of proof terms;

output physical_stderr, e.g. for low-level debugging;

tuned;

do not open ML structures;

tuned;

misc tuning -- slightly more readable;

simplified defs (thanks to Mohammad)

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;