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

new material; rotated premises of Lim_transform_eventually
2019-08-15, by paulson
clarified name context for abstractions -- in contrast to 367e60d9aa1b and Term.variant_frees (*as they are printed :-*);
2019-08-14, by wenzelm
tuned;
2019-08-14, by wenzelm
uniform standard_vars for terms and proof terms;
2019-08-14, by wenzelm
treat simproc results as atomic -- more compact proof terms;
2019-08-14, by wenzelm
tuned;
2019-08-13, by wenzelm
minor performance tuning;
2019-08-13, by wenzelm
NEWS and example for Theory.join_theory;
2019-08-13, by wenzelm
tuned whitespace;
2019-08-13, by wenzelm
more compact proof terms;
2019-08-13, by wenzelm
more documentation;
2019-08-13, by wenzelm
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
2019-08-13, by wenzelm
clarified modules;
2019-08-13, by wenzelm
merged
2019-08-12, by wenzelm
more compact proof terms;
2019-08-12, by wenzelm
more robust -- notably for metis, which tends to accumulate tpairs;
2019-08-12, by wenzelm
tuned -- avoid shadowing of ML names;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
more compact proof terms;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
tuned -- eliminated unused parameters;
2019-08-12, by wenzelm
more direct/compact export of proof terms;
2019-08-12, by wenzelm
output physical_stderr, e.g. for low-level debugging;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
do not open ML structures;
2019-08-12, by wenzelm
tuned;
2019-08-12, by wenzelm
misc tuning -- slightly more readable;
2019-08-12, by wenzelm
simplified defs (thanks to Mohammad)
2019-08-12, by nipkow
record sort constraints unconditionally: minimal performance implications;
2019-08-11, by wenzelm
more careful export of unnamed proof boxes: avoid duplicates via memoing;
2019-08-10, by wenzelm
tuned signature;
2019-08-10, by wenzelm
export each PThm node separately: slightly more scalable;
2019-08-10, by wenzelm
allow duplicate exports via strict = false;
2019-08-10, by wenzelm
tuned message;
2019-08-10, by wenzelm
more positions;
2019-08-10, by wenzelm
more positions;
2019-08-10, by wenzelm
tuned;
2019-08-09, by wenzelm
formal position for PThm nodes;
2019-08-09, by wenzelm
clarified ML types;
2019-08-09, by wenzelm
proper treatment of body oracles, outside of recursion into thms graph;
2019-08-09, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-08, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-08, by wenzelm
tuned whitespace -- slightly more readable;
2019-08-08, by wenzelm
clarified signature: fewer warnings in ML IDE;
2019-08-08, by wenzelm
tuned;
2019-08-08, by wenzelm
prefer named lemmas -- more compact proofterms;
2019-08-07, by wenzelm
more compact proofterms;
2019-08-07, by wenzelm
eliminated pointless comments;
2019-08-07, by wenzelm
clarified proofterms;
2019-08-07, by wenzelm
more robust and convenient treatment of implicit context;
2019-08-07, by wenzelm
removed junk (cf. fa933b98d64d);
2019-08-07, by wenzelm
explicit check of left-over constraints from different theory, e.g. due to lack of Thm.trim_context;
2019-08-07, by wenzelm
more careful treatment of implicit context;
2019-08-07, by wenzelm
more careful treatment of implicit context;
2019-08-07, by wenzelm
proper build options;
2019-08-07, by wenzelm
merged
2019-08-06, by wenzelm
backed out changeset 1b8858f4c393: odd problems e.g. in CAVA_LTL_Modelchecker;
2019-08-06, by wenzelm
more careful treatment of implicit context;
2019-08-06, by wenzelm
clarified signature;
2019-08-06, by wenzelm

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

isabelle