| Fri, 06 Dec 2024 23:07:09 +0100 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2024 22:16:29 +0100 |
wenzelm |
more elementary operation Term.variant_bounds: only for bounds vs. frees, no consts, no tfrees;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 21:01:59 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 19:21:38 +0100 |
wenzelm |
eliminate historic clone (see also 550e36c6a2d1);
|
file |
diff |
annotate
|
| Sat, 30 Nov 2024 17:14:30 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 11:26:17 +0100 |
wenzelm |
tuned: more standard Name.build_context, although that is a bit longer;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2024 00:25:03 +0100 |
wenzelm |
clarified signature: more uniform;
|
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
|
| Thu, 08 Aug 2024 16:23:30 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 16:56:28 +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
|
| Tue, 09 Jan 2024 15:14:49 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2024 22:53:38 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 08 Jan 2024 22:26:04 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 22:04:41 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 19:24:37 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2023 20:01:04 +0100 |
wenzelm |
eliminate clone (amending e7796c55d840);
|
file |
diff |
annotate
|
| Fri, 29 Dec 2023 19:05:10 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2023 22:11:13 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2023 21:31:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 20:17:13 +0100 |
wenzelm |
minor performance tuning;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 19:36:28 +0100 |
wenzelm |
revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 14:25:14 +0100 |
wenzelm |
minor performace tuning;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 14:05:19 +0100 |
wenzelm |
minor performance tuning: prefer Same.operation;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2023 13:40:02 +0100 |
wenzelm |
tuned: more standard accumulation;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 13:39:40 +0100 |
wenzelm |
more general Logic.incr_indexes_operation;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 12:18:22 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2023 11:56:56 +0100 |
wenzelm |
clarified ML;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 14:48:17 +0100 |
wenzelm |
tuned -- eliminate clones;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 13:09:39 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2023 12:05:56 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 15:25:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 12:12:13 +0100 |
wenzelm |
minor performance tuning: regular Same.operation;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 11:48:34 +0100 |
wenzelm |
clarified signature: more standard argument order;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 10:52:48 +0100 |
wenzelm |
tuned: more standard names;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 10:40:59 +0100 |
wenzelm |
tuned: prefer Same.commit;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2023 10:34:57 +0100 |
wenzelm |
tuned: more standard argument order;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2022 17:37:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2021 17:37:24 +0200 |
wenzelm |
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
|
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
|
| Mon, 04 Oct 2021 18:19:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 02 Oct 2021 12:45:51 +0200 |
wenzelm |
clarified Term.dest_abs (again, refining 71dfb835025d): only Free names are relevant for abstract terms, without syntax;
|
file |
diff |
annotate
|
| Sat, 02 Oct 2021 11:56:11 +0200 |
wenzelm |
tuned, following Syntax_Trans.variant_abs;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2021 16:54:21 +0100 |
wenzelm |
slightly more efficient Term.fastype_of (only little impact in regular applications);
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 14:32:59 +0100 |
wenzelm |
tuned signature -- eliminated clones;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 22:15:30 +0200 |
wenzelm |
more tight filtering;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 16:36:03 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 14:11:54 +0100 |
wenzelm |
avoid vacuous quantification, as usual for shared variable scope;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:17:49 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 21:49:02 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 13:42:58 +0200 |
wenzelm |
clarified abstracted term bindings (again, see c8384ff11711);
|
file |
diff |
annotate
|
| Sat, 30 May 2015 19:28:51 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 22:56:28 +0100 |
wenzelm |
discontinued legacy_isub_isup;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 17:26:22 +0200 |
wenzelm |
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 17:36:14 +0200 |
wenzelm |
more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;
|
file |
diff |
annotate
|