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 tip

merged
2023-04-24, by paulson
merged
2023-04-12, by paulson
merged
2023-03-20, by paulson
Numerous significant simplifications
2023-03-17, by paulson
stripped unused functionality
2023-05-02, by haftmann
tuned
2023-05-02, by haftmann
case translation in intermediate language eliminates semantic clone
2023-05-01, by haftmann
minor performance tuning;
2023-04-30, by wenzelm
more correct type calculation
2023-04-29, by haftmann
Backed out changeset 5016262a2384
2023-04-29, by haftmann
added lemma
2023-04-30, by nipkow
thingol: fix abstraction return types in case
2023-04-27, by stuebinm
merged
2023-04-27, by desharna
tuned; avoided intermediate lists
2023-04-27, by desharna
tuned; avoided intermediate list and list traversal
2023-04-27, by desharna
tuned; avoided intermediate lists
2023-04-27, by desharna
tuned; avoided intermediate list
2023-04-27, by desharna
made 'primcorec' more robust
2023-04-27, by blanchet
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
2023-04-26, by wenzelm
tuned signature;
2023-04-26, by wenzelm
more operations for lexicographic ordering;
2023-04-23, by wenzelm
more operations: following Library list operations and Ord_List.T operations;
2023-04-23, by wenzelm
tuned;
2023-04-23, by wenzelm
tuned;
2023-04-23, by wenzelm
tuned: concise combinators instead of bulky case-expressions;
2023-04-22, by wenzelm
provide ML antiquotation "if_none": non-strict version of "the_default";
2023-04-22, by wenzelm
merged
2023-04-22, by wenzelm
proper Thm.trim_context / Thm.transfer (see also 0d401f874942);
2023-04-21, by wenzelm
tuned;
2023-04-21, by wenzelm
more operations;
2023-04-21, by wenzelm
more operations;
2023-04-21, by wenzelm
more uniform operations wrt. Thm.full_prop_of;
2023-04-21, by wenzelm
proper Thm.trim_context / Thm.transfer for context data;
2023-04-21, by wenzelm
tuned: more concise data record;
2023-04-21, by wenzelm
tuned;
2023-04-21, by wenzelm
clarified counters and types;
2023-04-21, by wenzelm
tuned signature;
2023-04-20, by wenzelm
support n-ary merge theory data;
2023-04-20, by wenzelm
tuned;
2023-04-20, by wenzelm
tuned;
2023-04-20, by wenzelm
proper theory_long_name;
2023-04-20, by wenzelm
prefer theory_long_name in data;
2023-04-20, by wenzelm
proper theory_long_name;
2023-04-20, by wenzelm
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
2023-04-20, by wenzelm
tuned;
2023-04-19, by wenzelm
more operations, following Isabelle/ML conventions;
2023-04-19, by wenzelm
clarified theory_id: plain value without state;
2023-04-19, by wenzelm
tuned
2023-04-19, by haftmann
clarified terminology
2023-04-19, by haftmann
minor performance tuning: recursive check of pointer_eq;
2023-04-19, by wenzelm
minor performance tuning: avoid excessive (de)constructions for base cases;
2023-04-19, by wenzelm
unused (see also 864c7c684651 and b6aa5eac0a1a);
2023-04-19, by wenzelm
tuned;
2023-04-19, by wenzelm
tuned;
2023-04-18, by wenzelm
more operations: avoid intermediate list;
2023-04-18, by wenzelm
discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);
2023-04-18, by wenzelm
update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;
2023-04-18, by wenzelm
drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;
2023-04-18, by wenzelm
tuned;
2023-04-18, by wenzelm
backout b6aa5eac0a1a;
2023-04-18, by wenzelm

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

isabelle