isabelle: Graph

updated to jdk-17.0.7;
2023-05-09, by wenzelm
minor performance tuning (see also f906f7f83dae and b23c42b9f78a);
2023-05-09, by wenzelm
performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;
2023-05-09, by wenzelm
more operations;
2023-05-09, by wenzelm
tuned: more readable ML;
2023-05-09, by wenzelm
tuned;
2023-05-09, by wenzelm
backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms);
2023-05-09, by wenzelm
maintain dynamic position where values are created (again, amending afa6117bace4);
2023-05-09, by wenzelm
more robust: publish token only after assignment of result;
2023-05-09, by wenzelm
tuned comments;
2023-05-09, by wenzelm
clarified signature;
2023-05-09, by wenzelm
merged
2023-05-09, by wenzelm
tuned signature;
2023-05-09, by wenzelm
support for cached evaluation via weak_ref;
2023-05-08, by wenzelm
optional timing;
2023-05-08, by wenzelm
more informative trace of context allocations;
2023-05-08, by wenzelm
tuned;
2023-05-08, by wenzelm
tuned internal structure;
2023-05-08, by wenzelm
tuned;
2023-05-08, by wenzelm
tuned whitespace;
2023-05-08, by wenzelm
merged
2023-05-08, by desharna
added author
2023-05-08, by desharna
added lemma asymp_on_multpHO
2023-05-08, by desharna
added lemmas multpHO_iff_set_mset_lessHO_set_mset and multpHO_minus_inter_minus_inter_iff
2023-05-08, by desharna
added lemmas count_minus_inter_lt_count_minus_inter_iff and minus_inter_eq_minus_inter_iff
2023-05-08, by desharna
added lemma multpHO_implies_one_step_strong
2023-05-08, by desharna
merged
2023-05-07, by wenzelm
tuned comments;
2023-05-07, by wenzelm
tuned;
2023-05-07, by wenzelm
hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
2023-05-07, by wenzelm
minor performance tuning;
2023-05-07, by wenzelm
minor performance tuning;
2023-05-07, by wenzelm
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
2023-05-06, by wenzelm
tuned;
2023-05-06, by wenzelm
clarified data representation: slightly more compact, since internals_hidden is sparesely populated and rarely changes;
2023-05-06, by wenzelm
more operations;
2023-05-06, by wenzelm
more operations;
2023-05-06, by wenzelm
more operations;
2023-05-05, by wenzelm
minor performance tuning;
2023-05-05, by wenzelm
unused;
2023-05-05, by wenzelm
more complete accesses for "extern" operation, notably for aliases;
2023-05-05, by wenzelm
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
2023-05-05, by wenzelm
tuned;
2023-05-05, by wenzelm
tuned;
2023-05-05, by wenzelm
clarified signature;
2023-05-05, by wenzelm
unused;
2023-05-05, by wenzelm
minor performance tuning;
2023-05-05, by wenzelm
tuned signature;
2023-05-05, by wenzelm
minor performance tuning;
2023-05-05, by wenzelm
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;
2023-05-04, by wenzelm
tuned;
2023-05-04, by wenzelm
more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
2023-05-04, by wenzelm
tuned;
2023-05-03, by wenzelm
proper treatment of restriction (for 'qualified');
2023-05-03, by wenzelm
misc tuning;
2023-05-02, by wenzelm
more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;
2023-05-02, by wenzelm
more standard name bindings (amending 5bf71b4da706): avoid odd full_name like "Orderings.class.Orderings.preorder.of_class.intro" with many redundant name space accesses;
2023-05-02, by wenzelm
minor performance tuning: more compact representation of only sparsely table;
2023-05-02, by wenzelm
minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
2023-05-02, by wenzelm
proper checks;
2023-05-02, by wenzelm
tuned;
2023-05-02, by wenzelm
tuned structure;
2023-05-02, by wenzelm
tuned signature;
2023-05-02, by wenzelm
tuned;
2023-05-02, by wenzelm
clarified extern vs. alias/hide: output alternative names, if possible;
2023-05-01, by wenzelm
tuned;
2023-05-01, by wenzelm
minor performance tuning: more compact, more sharing;
2023-05-01, by wenzelm
potential performance tuning: more compact data structure, but less sharing;
2023-05-01, by wenzelm
Importation of additional lemmas from metric.ml
2023-05-07, by paulson
fixes esp to theory presentation
2023-05-06, by paulson
new material ported from HOL Light's metric.ml
2023-05-06, by paulson
merged
2023-05-04, by paulson
Two new theories containing material ported from HOL Light about abstract topology
2023-05-03, by paulson
merged
2023-05-04, by nipkow
streamlined
2023-05-04, by nipkow
merged
2023-05-03, by paulson
More new theorems, and a necessary correction
2023-05-02, by paulson
A few new theorems
2023-05-02, by paulson
merged
2023-05-02, 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
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
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