| 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
|
| Wed, 10 Jul 2013 16:25:26 +0200 |
wenzelm |
more robust identifier syntax: sub/superscript counts as modifier of LETDIG part instead of LETTER, both isub/isup and sub/sup are allowed;
|
file |
diff |
annotate
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2012 19:22:36 +0100 |
wenzelm |
support for sub-structured identifier syntax (inactive);
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 16:37:22 +0200 |
wenzelm |
report sort assignment of visible type variables;
|
file |
diff |
annotate
|
| Sun, 15 Jul 2012 17:53:47 +0200 |
wenzelm |
prefer canonical fold_rev;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|