wenzelm [Sun, 09 Jun 2024 21:15:27 +0200] rev 80312
more operations, following Isabelle/ML;
wenzelm [Sun, 09 Jun 2024 20:47:30 +0200] rev 80311
clarified signature: more explicit operations;
wenzelm [Sun, 09 Jun 2024 20:37:39 +0200] rev 80310
clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);
wenzelm [Sun, 09 Jun 2024 20:19:53 +0200] rev 80309
clarified operations, including exceptions;
wenzelm [Sun, 09 Jun 2024 20:04:41 +0200] rev 80308
tuned: more direct Isabelle/ML;
wenzelm [Sun, 09 Jun 2024 19:49:42 +0200] rev 80307
clarified modules;
wenzelm [Sun, 09 Jun 2024 15:31:33 +0200] rev 80306
more accurate thm "name_hint", using Thm_Name.T;
wenzelm [Sun, 09 Jun 2024 15:11:07 +0200] rev 80305
more operationsd;
wenzelm [Sun, 09 Jun 2024 12:29:04 +0200] rev 80304
tuned;
wenzelm [Sat, 08 Jun 2024 23:17:20 +0200] rev 80303
more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms);