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
|
Fri, 04 Jul 2025 15:08:09 +0100 |
paulson |
Two lemmas and a comment
|
changeset |
files
|
Thu, 03 Jul 2025 13:53:14 +0200 |
nipkow |
removed duplicate lemma; added the notion of the kernel of a function
|
changeset |
files
|
Tue, 01 Jul 2025 20:51:26 +0200 |
haftmann |
isabelle regenerate_cooper
|
changeset |
files
|
Mon, 30 Jun 2025 20:44:40 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
Mon, 30 Jun 2025 13:10:44 +0200 |
wenzelm |
obsolete (see 09904d5ef1f0);
|
changeset |
files
|
Mon, 30 Jun 2025 12:42:21 +0200 |
wenzelm |
inline errors as "bad" markup;
|
changeset |
files
|
Mon, 30 Jun 2025 11:28:04 +0200 |
wenzelm |
more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);
|
changeset |
files
|
Sun, 29 Jun 2025 16:16:22 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
changeset |
files
|
Sun, 29 Jun 2025 15:53:45 +0200 |
wenzelm |
more robust: avoid crash on session database errors;
|
changeset |
files
|
Sun, 29 Jun 2025 15:48:13 +0200 |
wenzelm |
tuned signature: more operations;
|
changeset |
files
|
Sun, 29 Jun 2025 14:17:49 +0200 |
wenzelm |
basic support to reload theory markup from session store;
|
changeset |
files
|
Sat, 28 Jun 2025 17:12:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 28 Jun 2025 16:24:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 28 Jun 2025 15:55:35 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 28 Jun 2025 15:45:55 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
Sat, 28 Jun 2025 12:27:43 +0200 |
wenzelm |
eliminate odd workaround from Aug-2012 (see 393a37003851);
|
changeset |
files
|
Sat, 28 Jun 2025 12:22:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 28 Jun 2025 12:17:48 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
Fri, 27 Jun 2025 15:31:55 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
Fri, 27 Jun 2025 15:03:12 +0200 |
wenzelm |
clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;
|
changeset |
files
|
Fri, 27 Jun 2025 14:52:01 +0200 |
wenzelm |
clarified signature: prefer private operation (see also 803731b62180);
|
changeset |
files
|
Fri, 27 Jun 2025 14:48:37 +0200 |
wenzelm |
tuned (see also 5c7652e9bc01);
|
changeset |
files
|
Fri, 27 Jun 2025 14:44:15 +0200 |
wenzelm |
tuned signature: more generic operations;
|
changeset |
files
|
Fri, 27 Jun 2025 14:41:18 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
Fri, 27 Jun 2025 13:44:36 +0200 |
wenzelm |
clarified signature: omit pointless object-oriented indirection;
|
changeset |
files
|
Fri, 27 Jun 2025 13:37:36 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|