wenzelm [Fri, 11 Jul 2025 14:03:09 +0200] rev 82842
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
wenzelm [Fri, 11 Jul 2025 12:04:31 +0200] rev 82841
tuned: order does not matter here;
wenzelm [Fri, 11 Jul 2025 11:59:22 +0200] rev 82840
clarified modules;
wenzelm [Fri, 11 Jul 2025 11:52:43 +0200] rev 82839
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
wenzelm [Thu, 10 Jul 2025 17:29:25 +0200] rev 82838
more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
avoid costly Item_Net.length, which is linear in size;
wenzelm [Thu, 10 Jul 2025 15:08:26 +0200] rev 82837
tuned proof;
wenzelm [Thu, 10 Jul 2025 12:40:45 +0200] rev 82836
clarified modules;
wenzelm [Wed, 09 Jul 2025 17:00:03 +0200] rev 82835
redundant: Net.DELETE already handled;
wenzelm [Wed, 09 Jul 2025 16:59:39 +0200] rev 82834
tuned;
wenzelm [Wed, 09 Jul 2025 12:48:44 +0200] rev 82833
clarified signature: more explicit types, notably (thm option) instead of (thm list);