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

More new theorems, and a necessary correction
24 months ago, by paulson
A few new theorems
24 months ago, by paulson
merged
24 months ago, by paulson
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
24 months ago, by haftmann
tuned
24 months ago, by haftmann
case translation in intermediate language eliminates semantic clone
24 months ago, by haftmann
minor performance tuning;
24 months ago, by wenzelm
more correct type calculation
24 months ago, by haftmann
Backed out changeset 5016262a2384
24 months ago, by haftmann
added lemma
24 months ago, by nipkow
thingol: fix abstraction return types in case
24 months ago, by stuebinm
merged
24 months ago, by desharna
tuned; avoided intermediate lists
24 months ago, by desharna
tuned; avoided intermediate list and list traversal
24 months ago, by desharna
tuned; avoided intermediate lists
24 months ago, by desharna
tuned; avoided intermediate list
24 months ago, by desharna
made 'primcorec' more robust
24 months ago, by blanchet
performance tuning: more balanced time vs. space tradeoff, notably for datatype package with its many name space operations;
24 months ago, 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

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

isabelle