| Mon, 14 Jul 2025 10:57:46 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Jul 2025 21:18:04 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Mon, 14 Jul 2025 18:41:41 +0100 |
paulson |
A few more lemmas
|
changeset |
files
|
| Mon, 14 Jul 2025 12:33:34 +0100 |
paulson |
A number of basic and unaccountably missing lemmas about complex exponentiation
|
changeset |
files
|
| Sun, 13 Jul 2025 17:29:48 +0100 |
paulson |
Lemmas about integrals and vector-valued functions
|
changeset |
files
|
| Sat, 12 Jul 2025 07:36:38 +0200 |
haftmann |
always use proper context when parsing constants
|
changeset |
files
|
| Sun, 13 Jul 2025 13:41:24 +0200 |
desharna |
tuned
|
changeset |
files
|
| Sat, 12 Jul 2025 22:37:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 12 Jul 2025 16:01:38 +0200 |
wenzelm |
proper thm ord that conforms to Thm.eq_thm_prop (amending f5fd9b41188a): relevant for declarations in a locale contex with assumptions, e.g. "locale test = assumes True begin declare refl [rule del] end";
|
changeset |
files
|
| Sat, 12 Jul 2025 13:05:04 +0200 |
wenzelm |
clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;
|
changeset |
files
|
| Fri, 11 Jul 2025 23:44:43 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Fri, 11 Jul 2025 23:36:13 +0200 |
wenzelm |
tuned comments: more formal sections;
|
changeset |
files
|
| 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);
|
changeset |
files
|
| Fri, 11 Jul 2025 21:39:03 +0200 |
wenzelm |
more robust: no failure on bad rule;
|
changeset |
files
|
| Fri, 11 Jul 2025 21:38:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 11 Jul 2025 21:36:22 +0200 |
wenzelm |
more accurate delete operation via authentic index --- minor performance tuning;
|
changeset |
files
|
| Fri, 11 Jul 2025 15:17:42 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Fri, 11 Jul 2025 15:01:33 +0200 |
wenzelm |
clarified signature: do not expose internal data structures;
|
changeset |
files
|
| Fri, 11 Jul 2025 14:55:49 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Fri, 11 Jul 2025 14:37:23 +0200 |
wenzelm |
clarified signature: prefer canonical order (latest declarations first);
|
changeset |
files
|
| Fri, 11 Jul 2025 14:12:55 +0200 |
wenzelm |
clarified print order: follow original classical.ML, before 8aa1c98b948b;
|
changeset |
files
|
| Fri, 11 Jul 2025 14:03:09 +0200 |
wenzelm |
maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;
|
changeset |
files
|
| Fri, 11 Jul 2025 12:04:31 +0200 |
wenzelm |
tuned: order does not matter here;
|
changeset |
files
|
| Fri, 11 Jul 2025 11:59:22 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Fri, 11 Jul 2025 11:52:43 +0200 |
wenzelm |
clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Thu, 10 Jul 2025 15:08:26 +0200 |
wenzelm |
tuned proof;
|
changeset |
files
|
| Thu, 10 Jul 2025 12:40:45 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Wed, 09 Jul 2025 17:00:03 +0200 |
wenzelm |
redundant: Net.DELETE already handled;
|
changeset |
files
|
| Wed, 09 Jul 2025 16:59:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 09 Jul 2025 12:48:44 +0200 |
wenzelm |
clarified signature: more explicit types, notably (thm option) instead of (thm list);
|
changeset |
files
|
| Wed, 09 Jul 2025 11:42:52 +0200 |
wenzelm |
more robust: unique result expected, otherwise index calculations will go wrong;
|
changeset |
files
|
| Wed, 09 Jul 2025 11:28:56 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 09 Jul 2025 11:22:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 09 Jul 2025 11:09:00 +0200 |
wenzelm |
clarified signature: anticipate use in src/Provers/classical.ML;
|
changeset |
files
|
| Tue, 08 Jul 2025 12:10:00 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 08 Jul 2025 12:06:21 +0200 |
wenzelm |
tuned source structure;
|
changeset |
files
|
| Mon, 07 Jul 2025 22:11:44 +0200 |
wenzelm |
efficient rule declarations in canonical order, for update of netpairs and print operation;
|
changeset |
files
|
| Fri, 11 Jul 2025 10:12:01 +0200 |
desharna |
added option `-S` to Mirabelle to specify the subgoal classes to consider
|
changeset |
files
|
| Tue, 08 Jul 2025 19:13:44 +0200 |
haftmann |
moved to more appropriate theory
|
changeset |
files
|
| Sun, 06 Jul 2025 10:01:32 +0200 |
haftmann |
more correct lemma name
|
changeset |
files
|
| Tue, 08 Jul 2025 14:42:35 +0200 |
desharna |
merged
|
changeset |
files
|
| Tue, 08 Jul 2025 14:27:09 +0200 |
desharna |
added basic support for persistent prover data to Sledgehammer
|
changeset |
files
|
| Sun, 06 Jul 2025 15:26:59 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 06 Jul 2025 14:59:48 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sun, 06 Jul 2025 14:58:00 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Sun, 06 Jul 2025 14:53:20 +0200 |
wenzelm |
clarified signature: more explicit type Bires.kind;
|
changeset |
files
|
| Sun, 06 Jul 2025 13:58:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 06 Jul 2025 12:06:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 06 Jul 2025 11:43:34 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sun, 06 Jul 2025 11:35:18 +0200 |
wenzelm |
proper weight, instead of magic number 1000000 (see b3f190995bc9);
|
changeset |
files
|
| Sun, 06 Jul 2025 11:33:23 +0200 |
wenzelm |
just one type Bires.netpair, based on Bires.tag with explicit weight;
|
changeset |
files
|
| Sat, 05 Jul 2025 16:19:23 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 05 Jul 2025 16:12:48 +0200 |
wenzelm |
tuned signature: do not expose private operation;
|
changeset |
files
|
| Sat, 05 Jul 2025 16:01:40 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|
| Sat, 05 Jul 2025 15:53:52 +0200 |
wenzelm |
clarified modules;
|
changeset |
files
|
| Sat, 05 Jul 2025 15:03:26 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sat, 05 Jul 2025 14:39:24 +0200 |
wenzelm |
tuned signature: more explicit types;
|
changeset |
files
|
| Sat, 05 Jul 2025 14:19:45 +0200 |
wenzelm |
clarified modules: explicit structure Bires;
|
changeset |
files
|
| Thu, 03 Jul 2025 15:28:31 +0200 |
wenzelm |
minor performance tuning;
|
changeset |
files
|