| Fri, 25 Apr 2025 11:22:25 +0200 |
wenzelm |
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 20:12:45 +0100 |
wenzelm |
clarified signature (see also 2157039256d3);
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 23:48:45 +0100 |
wenzelm |
commands 'syntax_types' and 'syntax_consts' now work in a local theory context;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2024 21:47:20 +0100 |
wenzelm |
syntax translations now work in a local theory context;
|
file |
diff |
annotate
|
| Sun, 08 Dec 2024 20:09:14 +0100 |
wenzelm |
more markup (without rendering): class, type constructor, term constant --- similar to free, bound, etc.;
|
file |
diff |
annotate
|
| Sat, 07 Dec 2024 23:50:18 +0100 |
wenzelm |
clarified term positions and markup: syntax = true means this is via concrete syntax;
|
file |
diff |
annotate
|
| Fri, 06 Dec 2024 13:33:25 +0100 |
wenzelm |
clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 18:53:45 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 14:30:10 +0100 |
wenzelm |
more accurate extern_const: avoid clash with frees;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 14:08:28 +0100 |
wenzelm |
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 11:36:53 +0100 |
wenzelm |
clarified signature: uniform context;
|
file |
diff |
annotate
|
| Sun, 01 Dec 2024 22:14:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 24 Oct 2024 22:05:57 +0200 |
wenzelm |
prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);
|
file |
diff |
annotate
|
| Tue, 22 Oct 2024 21:29:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Oct 2024 19:26:40 +0200 |
wenzelm |
more concise representation of term positions;
|
file |
diff |
annotate
|
| Mon, 21 Oct 2024 22:28:07 +0200 |
wenzelm |
notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
|
file |
diff |
annotate
|
| Mon, 21 Oct 2024 20:02:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 21 Oct 2024 14:50:59 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 05 Oct 2024 14:58:36 +0200 |
wenzelm |
first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2024 14:33:03 +0200 |
wenzelm |
proper fbreaks (amending 53f12ab896e6);
|
file |
diff |
annotate
|
| Fri, 20 Sep 2024 14:28:13 +0200 |
wenzelm |
clarified signature: more explicit operations;
|
file |
diff |
annotate
|
| Tue, 17 Sep 2024 17:51:55 +0200 |
wenzelm |
more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 20:21:04 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Fri, 23 Aug 2024 14:56:33 +0200 |
wenzelm |
clarified markup: more uniform;
|
file |
diff |
annotate
|
| Thu, 22 Aug 2024 15:57:30 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 12:21:13 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Mon, 10 Jun 2024 14:29:33 +0200 |
wenzelm |
more robust / permissive;
|
file |
diff |
annotate
|
| Mon, 10 Jun 2024 14:05:39 +0200 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Mon, 10 Jun 2024 12:44:49 +0200 |
wenzelm |
clarified operations, following pretty_thm_name;
|
file |
diff |
annotate
|
| Sun, 09 Jun 2024 19:49:42 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 08 Jun 2024 16:26:47 +0200 |
wenzelm |
more accurate output of Thm_Name.T wrt. facts name space;
|
file |
diff |
annotate
|
| Tue, 02 Apr 2024 18:29:14 +0200 |
wenzelm |
clarified names: discontinue odd convention from 3 decades ago;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 14:36:29 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:43:10 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:37:29 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2024 13:10:20 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 22:40:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 17:10:09 +0100 |
wenzelm |
misc tuning and clarification: prefer Same.operation;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 16:04:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2024 12:18:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2024 21:53:27 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 16:10:10 +0100 |
wenzelm |
more accurate Global_Theory.name_facts: burrow into expression of attributed theorems;
|
file |
diff |
annotate
|
| Wed, 27 Dec 2023 13:17:55 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 24 Dec 2023 12:23:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 24 Dec 2023 11:13:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 17:42:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 May 2023 16:12:37 +0200 |
wenzelm |
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
|
file |
diff |
annotate
|
| Mon, 15 May 2023 14:13:58 +0200 |
wenzelm |
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
|
file |
diff |
annotate
|
| Sat, 06 May 2023 23:20:20 +0200 |
wenzelm |
back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
|
file |
diff |
annotate
|
| Fri, 05 May 2023 15:56:12 +0200 |
wenzelm |
more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 21:48:47 +0200 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 23:15:02 +0200 |
wenzelm |
localized command 'syntax' and 'no_syntax';
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 21:56:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 20:43:38 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 13 May 2021 15:52:10 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 02 May 2021 17:38:49 +0200 |
wenzelm |
support nested cases;
|
file |
diff |
annotate
|
| Wed, 27 May 2020 20:02:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|