| Sun, 31 Dec 2023 19:24:37 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2023 22:36:41 +0100 |
wenzelm |
clarified signature: more operations;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2023 15:36:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 25 Oct 2021 17:40:49 +0200 |
wenzelm |
tuned;
|
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
|
| Mon, 25 Oct 2021 17:26:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 13:49:26 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 19:56:03 +0200 |
wenzelm |
tuned;
|
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:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 22:39:39 +0200 |
wenzelm |
clarified standardization of variables, with proper treatment of local variables;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 20:31:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 21 Feb 2018 18:41:41 +0100 |
wenzelm |
explicit operations to instantiate frees: typ, term, thm, morphism;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 21:34:11 +0100 |
wenzelm |
more scalable zero_var_indexes, depending on canonical order within table;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 13:46:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 13:39:05 +0200 |
wenzelm |
removed unused "option" variants of "same" operations;
|
file |
diff |
annotate
|
| Tue, 04 May 2010 12:30:15 +0200 |
wenzelm |
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 23:13:01 +0100 |
wenzelm |
modernized structure Term_Ord;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 21:00:09 +0200 |
wenzelm |
use structure Same;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 17:03:11 +0200 |
wenzelm |
use structure Same;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 00:08:38 +0200 |
wenzelm |
added some generic mapping combinators;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:32 +0100 |
wenzelm |
zero_var_indexes_inst: multiple terms;
|
file |
diff |
annotate
|
| Sun, 12 Nov 2006 21:14:52 +0100 |
wenzelm |
instantiate: tuned indentity case;
|
file |
diff |
annotate
|
| Sun, 05 Nov 2006 21:44:39 +0100 |
wenzelm |
instantiate: avoid global references;
|
file |
diff |
annotate
|