| Mon, 10 Apr 2023 18:08:23 +0200 | wenzelm | performance tuning: replace Ord_List by Set(); | changeset | files |
| Mon, 10 Apr 2023 14:59:40 +0200 | wenzelm | performance tuning: make_size accounts for boxes, i.e. pointer derefs required in "count"; | changeset | files |
| Mon, 10 Apr 2023 14:13:48 +0200 | wenzelm | NEWS; | changeset | files |
| Mon, 10 Apr 2023 13:43:11 +0200 | wenzelm | performance tuning; | changeset | files |
| Sun, 09 Apr 2023 23:09:24 +0200 | 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; | changeset | files |
| Sun, 09 Apr 2023 19:10:01 +0200 | wenzelm | proper stmt.execute() within loop (amending 9d9b30741fc4); | changeset | files |
| Sun, 09 Apr 2023 18:32:39 +0200 | wenzelm | clarified signature; | changeset | files |