| Fri, 06 Dec 2024 20:26:33 +0100 |
wenzelm |
clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with 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
|
| Sun, 01 Dec 2024 14:01:47 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 22:33:21 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 22:02:36 +0100 |
wenzelm |
tuned names/scopes;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 21:01:59 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 13:41:38 +0100 |
wenzelm |
tuned: more direct use of Name.context operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 00:25:03 +0100 |
wenzelm |
clarified signature: more uniform;
|
file |
diff |
annotate
|
| Thu, 28 Nov 2024 19:35:30 +0100 |
wenzelm |
omit redundant combinators (amending 7456a64bc4f6);
|
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
|
| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
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
|
| Tue, 02 May 2023 11:11:19 +0200 |
wenzelm |
proper checks;
|
file |
diff |
annotate
|
| Mon, 18 Oct 2021 11:40:57 +0200 |
wenzelm |
more robust Variable.revert_bounds (see also b12f2cef3ee5);
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 20:21:13 +0200 |
wenzelm |
more accurate treatment of context;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 23:07:02 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 11:32:18 +0200 |
wenzelm |
more efficient operations: traverse hyps only when required;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2021 23:21:32 +0200 |
wenzelm |
more robust signature: result has no particular order;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 18:21:58 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:57:33 +0200 |
wenzelm |
more scalable data structure (but: rarely used many arguments);
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:52:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| Thu, 19 Dec 2019 15:22:35 +0100 |
wenzelm |
more robust bound_fixes: external name does appear in "fixes" name space and could clash with direct fixes (e.g. via Subgoal.FOCUS within a global context);
|
file |
diff |
annotate
|
| Thu, 19 Dec 2019 14:46:10 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 13:43:17 +0200 |
wenzelm |
more compact XML: separate environment for free variables;
|
file |
diff |
annotate
|