wenzelm [Fri, 11 Jul 2025 23:44:43 +0200] rev 82853
tuned source structure;
wenzelm [Fri, 11 Jul 2025 23:36:13 +0200] rev 82852
tuned comments: more formal sections;
wenzelm [Fri, 11 Jul 2025 23:03:49 +0200] rev 82851
proper "plain" rule for extra_netpair (amending 8aa1c98b948b): need to avoid flat_rule / Object_Logic.atomize_prems for the sake of "standard" Isar proof, e.g. (line 34 of "$AFP/AWN/Qmsg_Lifting.thy);
wenzelm [Fri, 11 Jul 2025 21:39:03 +0200] rev 82850
more robust: no failure on bad rule;
wenzelm [Fri, 11 Jul 2025 21:38:14 +0200] rev 82849
tuned;
wenzelm [Fri, 11 Jul 2025 21:36:22 +0200] rev 82848
more accurate delete operation via authentic index --- minor performance tuning;
wenzelm [Fri, 11 Jul 2025 15:17:42 +0200] rev 82847
minor performance tuning;
wenzelm [Fri, 11 Jul 2025 15:01:33 +0200] rev 82846
clarified signature: do not expose internal data structures;
wenzelm [Fri, 11 Jul 2025 14:55:49 +0200] rev 82845
clarified signature;
wenzelm [Fri, 11 Jul 2025 14:37:23 +0200] rev 82844
clarified signature: prefer canonical order (latest declarations first);