| 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
|
| Tue, 12 Sep 2006 12:16:17 +0200 |
wenzelm |
Efficient term substitution -- avoids copying.
|
file |
diff |
annotate
|