isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

simplified proofs
2019-08-29, by nipkow
more rules for ordered real vector spaces
2019-08-29, by haftmann
simplified setup
2019-08-29, by nipkow
tuned proof
2019-08-29, by nipkow
merged
2019-08-28, by wenzelm
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;
2019-08-28, by wenzelm
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
2019-08-28, by wenzelm
more scalable -- less ML heap requirements;
2019-08-28, by wenzelm
tuned whitespace;
2019-08-28, by wenzelm
Integrate locale activation fallback diagnostics with 'trace_locales'.
2019-08-28, by ballarin
entry point for analysis without integration theory
2019-08-28, by immler
removed Brouwer_Fixpoint from imports of Derivative
2019-08-28, by immler
removed unused lemma, generalized, reduced dependencies
2019-08-27, by immler
fixed typo
2019-08-27, by immler
moved lemmas; reduced dependencies of Lipschitz
2019-08-27, by immler
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
2019-08-27, by immler
merged
2019-08-27, by nipkow
moved lemmas
2019-08-27, by nipkow
moved basic theorem
2019-08-27, by immler
proper positions for 'termination' command (see also 5549e686d6ac);
2019-08-27, by wenzelm
tuned names -- proper scopes;
2019-08-27, by wenzelm
added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);
2019-08-26, by wenzelm
proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;
2019-08-25, by wenzelm
Tracing of locale activation.
2019-08-24, by ballarin
tuned
2019-08-23, by nipkow
always export Pure proofs;
2019-08-23, by wenzelm
clarified 'thm_deps' command;
2019-08-23, by wenzelm
more compact: avoid pointless PThm rudiments;
2019-08-23, by wenzelm
clarified signature: prefer total operations;
2019-08-23, by wenzelm
proper graph traversal: avoid multiple visit of unnamed nodes;
2019-08-21, by wenzelm
more scalable: avoid huge intermediate XML elems;
2019-08-21, by wenzelm
more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
2019-08-21, by wenzelm
NEWS;
2019-08-20, by wenzelm
merged
2019-08-20, by wenzelm
export thm_deps;
2019-08-20, by wenzelm
proper theory context;
2019-08-20, by wenzelm
clarified thm_id vs. thm_node/thm: retain theory_name;
2019-08-20, by wenzelm
clarified signature;
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
unused (see 095dadc62bb5);
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
tuned signature;
2019-08-20, by wenzelm
clarified modules;
2019-08-20, by wenzelm
clarified modules;
2019-08-20, by wenzelm
tuned;
2019-08-20, by wenzelm
clarified signature;
2019-08-20, by wenzelm
tuned
2019-08-20, by nipkow
tuned
2019-08-20, by nipkow
merged
2019-08-20, by nipkow
tuned
2019-08-20, by nipkow
merged
2019-08-19, by wenzelm
clarified signature;
2019-08-19, by wenzelm
clarified export of axioms and theorems (identified derivations instead of projected facts);
2019-08-19, by wenzelm
tuned signature;
2019-08-19, by wenzelm
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
2019-08-19, by wenzelm
module Thm_Name for Isabelle/Scala;
2019-08-19, by wenzelm
tuned;
2019-08-19, by wenzelm
clarified modules;
2019-08-19, by wenzelm
tuned;
2019-08-19, by wenzelm
tuned
2019-08-19, by nipkow

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle