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
|
Fri, 27 Jun 2025 13:24:05 +0200 |
wenzelm |
tuned: avoid overlapping scopes;
|
changeset |
files
|
Fri, 27 Jun 2025 12:25:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Fri, 27 Jun 2025 08:09:26 +0200 |
haftmann |
typo
|
changeset |
files
|
Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
append (rather than prepend) code equations: the order within a theory is maintained in the resulting code
|
changeset |
files
|
Thu, 26 Jun 2025 17:25:29 +0200 |
haftmann |
scope pending code equations to theories
|
changeset |
files
|
Thu, 26 Jun 2025 17:30:33 +0200 |
nipkow |
merged
|
changeset |
files
|
Thu, 26 Jun 2025 17:30:16 +0200 |
nipkow |
tuned
|
changeset |
files
|
Thu, 26 Jun 2025 17:16:14 +0200 |
wenzelm |
enforce rebuild of Isabelle/ML;
|
changeset |
files
|
Thu, 26 Jun 2025 17:14:01 +0200 |
wenzelm |
proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);
|
changeset |
files
|
Wed, 25 Jun 2025 16:35:25 +0200 |
wenzelm |
merged
|
changeset |
files
|
Wed, 25 Jun 2025 13:32:28 +0200 |
wenzelm |
more operations (e.g. for testing);
|
changeset |
files
|
Wed, 25 Jun 2025 13:29:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Wed, 25 Jun 2025 13:16:07 +0200 |
wenzelm |
tuned signature: more explicit operations;
|
changeset |
files
|
Wed, 25 Jun 2025 12:51:35 +0200 |
wenzelm |
more accurate ML_Settings from underlying Session;
|
changeset |
files
|
Wed, 25 Jun 2025 12:43:37 +0200 |
wenzelm |
more accurate ML_Settings from underlying Session;
|
changeset |
files
|