2023-04-11 wenzelm performance tuning: replace Table() by Set();
2023-04-11 wenzelm minor performance tuning: more compact persistent data;
2023-04-11 wenzelm performance tuning: replace Table() by Set();
2023-04-11 wenzelm tuned;
2023-04-11 wenzelm more operations;
2023-04-11 wenzelm unused (see 34dd96a06c45);
2023-04-11 wenzelm more compact data: approx. 75% .. 85% of AList size;
2023-04-11 wenzelm tuned;
2023-04-11 haftmann some remarks on division
2023-04-11 haftmann proper section headings
2023-04-10 wenzelm more NEWS;
2023-04-10 wenzelm clarified NEWS;
2023-04-10 wenzelm performance tuning: replace Ord_List by Set();
2023-04-10 wenzelm tuned;
2023-04-10 wenzelm performance tuning: replace Ord_List by Table();
2023-04-10 wenzelm more Set() and Table() instances;
2023-04-10 wenzelm tuned;
2023-04-10 wenzelm performance tuning: replace Ord_List by Set();
2023-04-10 wenzelm performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count";
2023-04-10 wenzelm NEWS;
2023-04-10 wenzelm performance tuning;
2023-04-09 wenzelm more robust: avoid crash of Build_Log.parse_build_info / Protocol.Error_Message_Marker, e.g. in session MDP-Rewards of Isabelle/26ec258e5cf8 + AFP/2859e11cc09b;
2023-04-09 wenzelm proper stmt.execute() within loop (amending 9d9b30741fc4);
2023-04-09 wenzelm clarified signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 tip