isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +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;
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
tuned;
2023-04-18, by wenzelm
Thm.shared context: speed-up low-level inferences;
2023-04-18, by wenzelm
tuned whitespace;
2023-04-18, by wenzelm
backout 4a174bea55e2;
2023-04-18, by wenzelm
Backed out changeset f34d11942ac1
2023-04-18, by wenzelm
backout e3fe192fa4a8;
2023-04-18, by wenzelm
backout 61f652dd955a;
2023-04-18, by wenzelm
Backed out changeset e3db27e3b0c6
2023-04-18, by wenzelm
Backed out changeset cd5d56abda10
2023-04-18, by wenzelm
revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
2023-04-17, by wenzelm
merged
2023-04-15, by wenzelm
tuned;
2023-04-15, by wenzelm
merged
2023-04-15, by Lars Hupel
code_target: create subdirectories for export_code file
2023-04-04, by stuebinm
clarified signature: support "suppress" prefix as int, followed by list;
2023-04-15, by wenzelm
minor performance tuning: more elementary operations;
2023-04-15, by wenzelm
tuned signature;
2023-04-15, by wenzelm
minor performance tuning: more elementary operations;
2023-04-15, by wenzelm
tuned signature;
2023-04-15, by wenzelm
more operations;
2023-04-15, by wenzelm
more direct hg_sync init via ssh (see also 721b3278c8e4);
2023-04-14, by wenzelm
tuned;
2023-04-14, by wenzelm
more operations;
2023-04-14, by wenzelm
tuned: more direct re-use;
2023-04-14, by wenzelm
more direct clone (see also change of exception in 8d8c70b41bab);
2023-04-14, by wenzelm
more operations, following Isabelle/ML conventions;
2023-04-14, by wenzelm
more operations, following Isabelle/ML conventions;
2023-04-14, by wenzelm
proforma use of Long_Name.chunks, without change of the representation of accesses yet;
2023-04-14, by wenzelm
merged
2023-04-14, by wenzelm
minor performance tuning;
2023-04-13, by wenzelm
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
2023-04-13, by wenzelm
clarified signature;
2023-04-13, by wenzelm
misc tuning and clarification;
2023-04-12, by wenzelm
more compact: avoid redundant entries;
2023-04-12, by wenzelm
tuned;
2023-04-12, by wenzelm
tuned;
2023-04-12, by wenzelm
more operations;
2023-04-12, by wenzelm
performance tuning: proper pointer_eq;
2023-04-12, by wenzelm
added lemmas multpHO_repeat_mset_repeat_mset[simp] and multpHO_double_double[simp]
2023-04-13, by desharna
merged
2023-04-13, by desharna
added lemma multp_image_mset_image_msetI
2023-04-12, by desharna
merged
2023-04-13, by nipkow
proper invariants
2023-04-13, by nipkow
merged
2023-04-12, by wenzelm
misc tuning: follow Table() more closely;
2023-04-11, by wenzelm
tuned signature;
2023-04-11, by wenzelm
tuned;
2023-04-11, by wenzelm
performance tuning: replace Ord_List by Table();
2023-04-11, by wenzelm
performance tuning: replace Ord_List by Set();
2023-04-11, by wenzelm
tuned;
2023-04-11, by wenzelm
more operations;
2023-04-11, by wenzelm
tuned;
2023-04-11, by wenzelm
performance tuning: replace Table() by Set();
2023-04-11, by wenzelm
minor performance tuning: more compact persistent data;
2023-04-11, by wenzelm
performance tuning: replace Table() by Set();
2023-04-11, by wenzelm
tuned;
2023-04-11, by wenzelm
more operations;
2023-04-11, by wenzelm