| Sun, 20 Jul 2025 19:06:21 +0200 |
wenzelm |
more robust treatment of impossible case;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 14:24:21 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 12:40:08 +0200 |
wenzelm |
clarified signature: more uniform;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 12:37:50 +0200 |
wenzelm |
clarified messages;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 11:56:24 +0200 |
wenzelm |
more accurate warning;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 11:26:31 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 15 Jul 2025 10:48:45 +0200 |
wenzelm |
explicit "dest" rules: no longer declare [elim_format, elim];
|
file |
diff |
annotate
|
| Mon, 14 Jul 2025 12:23:32 +0200 |
wenzelm |
avoid redundant argument (amending af6f55b15749);
|
file |
diff |
annotate
|
| Mon, 14 Jul 2025 11:46:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2025 11:18:10 +0200 |
wenzelm |
clarified output;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2025 10:57:46 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 23:44:43 +0200 |
wenzelm |
tuned source structure;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 23:36:13 +0200 |
wenzelm |
tuned comments: more formal sections;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 23:03:49 +0200 |
wenzelm |
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);
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 21:38:14 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 21:36:22 +0200 |
wenzelm |
more accurate delete operation via authentic index --- minor performance tuning;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 15:01:33 +0200 |
wenzelm |
clarified signature: do not expose internal data structures;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 14:55:49 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 14:03:09 +0200 |
wenzelm |
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 12:04:31 +0200 |
wenzelm |
tuned: order does not matter here;
|
file |
diff |
annotate
|
| Fri, 11 Jul 2025 11:59:22 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 10 Jul 2025 17:29:25 +0200 |
wenzelm |
more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation;
|
file |
diff |
annotate
|
| Wed, 09 Jul 2025 12:48:44 +0200 |
wenzelm |
clarified signature: more explicit types, notably (thm option) instead of (thm list);
|
file |
diff |
annotate
|
| Wed, 09 Jul 2025 11:42:52 +0200 |
wenzelm |
more robust: unique result expected, otherwise index calculations will go wrong;
|
file |
diff |
annotate
|
| Wed, 09 Jul 2025 11:28:56 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 09 Jul 2025 11:22:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 06 Jul 2025 14:58:00 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sun, 06 Jul 2025 12:06:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 06 Jul 2025 11:43:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 06 Jul 2025 11:35:18 +0200 |
wenzelm |
proper weight, instead of magic number 1000000 (see b3f190995bc9);
|
file |
diff |
annotate
|
| Sun, 06 Jul 2025 11:33:23 +0200 |
wenzelm |
just one type Bires.netpair, based on Bires.tag with explicit weight;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2025 16:01:40 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2025 15:53:52 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2025 15:03:26 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2025 14:39:24 +0200 |
wenzelm |
tuned signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2025 14:19:45 +0200 |
wenzelm |
clarified modules: explicit structure Bires;
|
file |
diff |
annotate
|
| Thu, 03 Jul 2025 15:28:31 +0200 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 09 Apr 2016 21:42:42 +0200 |
wenzelm |
removed old proof method "default";
|
file |
diff |
annotate
|
| Wed, 16 Dec 2015 16:31:36 +0100 |
wenzelm |
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 18:03:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 20:57:34 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 20:17:35 +0200 |
wenzelm |
store result of swapify, to avoid later access to implicit context;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 13:08:00 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 15:36:06 +0200 |
wenzelm |
delete precisely the added rules;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 14:48:37 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 11:55:21 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 11:46:08 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 11:29:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 18:59:15 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 21:44:18 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 22:48:26 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 15:41:11 +0200 |
wenzelm |
no arguments for "standard" (or old "default") methods;
|
file |
diff |
annotate
|
| Tue, 30 Jun 2015 15:20:56 +0200 |
wenzelm |
renamed "default" to "standard", to make semantically clear what it is;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|