| Sun, 27 Jul 2025 16:28:10 +0200 |
wenzelm |
more direct support for "command_span" markup property "is_begin";
|
changeset |
files
|
| Sun, 27 Jul 2025 14:58:34 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Sun, 27 Jul 2025 14:53:30 +0200 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sun, 27 Jul 2025 13:49:05 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Thu, 24 Jul 2025 17:46:29 +0200 |
haftmann |
clarified code setup
|
changeset |
files
|
| Thu, 24 Jul 2025 16:44:52 +0200 |
haftmann |
moved / rearranged lemma
|
changeset |
files
|
| Wed, 23 Jul 2025 13:22:58 +0200 |
haftmann |
eliminate code drop: declarations where none needed
|
changeset |
files
|
| Wed, 23 Jul 2025 13:22:51 +0200 |
haftmann |
internal setting to identify pointless code drop: declarations
|
changeset |
files
|
| Wed, 23 Jul 2025 14:53:21 +0200 |
wenzelm |
clarified colors, following d6a14ed060fb;
|
changeset |
files
|
| Wed, 23 Jul 2025 13:21:52 +0200 |
wenzelm |
more comments;
|
changeset |
files
|
| Wed, 23 Jul 2025 13:10:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 23 Jul 2025 13:05:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 22 Jul 2025 12:02:53 +0200 |
wenzelm |
back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;
|
changeset |
files
|
| Tue, 22 Jul 2025 11:55:42 +0200 |
wenzelm |
proper default colors (amending e840461d5370): e.g. relevant for session_graph.pdf;
|
changeset |
files
|
| Mon, 21 Jul 2025 16:21:37 +0200 |
wenzelm |
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
|
changeset |
files
|
| Mon, 21 Jul 2025 15:10:00 +0200 |
wenzelm |
clarified natural decl_ord vs. slightly odd merge_decl_ord, following the historic status-quo of 53e56e6a67c3, which originally stems from c06d01f75764;
|
changeset |
files
|
| Mon, 21 Jul 2025 12:57:58 +0200 |
wenzelm |
clarified merge order: accurately reproduce the stable status-quo from 53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of AFP/f1299d4f896c;
|
changeset |
files
|
| Sun, 20 Jul 2025 21:50:07 +0200 |
wenzelm |
clarified decl_ord wrt. kind_ord;
|
changeset |
files
|
| Sun, 20 Jul 2025 20:31:04 +0200 |
wenzelm |
more diagnostic operations;
|
changeset |
files
|
| Sun, 20 Jul 2025 19:06:21 +0200 |
wenzelm |
more robust treatment of impossible case;
|
changeset |
files
|
| Sat, 19 Jul 2025 18:41:55 +0200 |
haftmann |
clarified name and status of auxiliary operation
|
changeset |
files
|
| Thu, 17 Jul 2025 21:06:22 +0100 |
nipkow |
moved lemma
|
changeset |
files
|
| Thu, 17 Jul 2025 20:09:42 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 16 Jul 2025 08:40:24 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 16 Jul 2025 08:40:18 +0100 |
paulson |
Complex analysis lemmas
|
changeset |
files
|
| Tue, 15 Jul 2025 23:13:12 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 15 Jul 2025 22:05:06 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 15 Jul 2025 14:25:30 +0200 |
wenzelm |
more robust, for typical error message prefix/suffix;
|
changeset |
files
|
| Tue, 15 Jul 2025 14:24:21 +0200 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Tue, 15 Jul 2025 12:45:52 +0200 |
wenzelm |
NEWS;
|
changeset |
files
|
| Tue, 15 Jul 2025 12:40:08 +0200 |
wenzelm |
clarified signature: more uniform;
|
changeset |
files
|
| Tue, 15 Jul 2025 12:37:50 +0200 |
wenzelm |
clarified messages;
|
changeset |
files
|
| Tue, 15 Jul 2025 11:56:24 +0200 |
wenzelm |
more accurate warning;
|
changeset |
files
|
| Tue, 15 Jul 2025 11:26:31 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 15 Jul 2025 11:22:02 +0200 |
wenzelm |
tuned (see also 9e7d1c139569);
|
changeset |
files
|
| Tue, 15 Jul 2025 11:11:56 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Jul 2025 11:27:59 +0200 |
wenzelm |
clarified signature;
|
changeset |
files
|
| Tue, 15 Jul 2025 11:04:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Jul 2025 10:48:45 +0200 |
wenzelm |
explicit "dest" rules: no longer declare [elim_format, elim];
|
changeset |
files
|
| Mon, 14 Jul 2025 22:58:27 +0200 |
wenzelm |
more accurate declarations;
|
changeset |
files
|
| Mon, 14 Jul 2025 12:23:32 +0200 |
wenzelm |
avoid redundant argument (amending af6f55b15749);
|
changeset |
files
|
| Mon, 14 Jul 2025 11:46:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 14 Jul 2025 11:18:10 +0200 |
wenzelm |
clarified output;
|
changeset |
files
|
| 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
|