| 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 |