Sat, 24 May 2008 20:05:21 +0200 use: explicit .ML;
wenzelm [Sat, 24 May 2008 20:05:21 +0200] rev 26981
use: explicit .ML;
Sat, 24 May 2008 14:47:43 +0200 ident: naive caching prevents potentially slow external invocations;
wenzelm [Sat, 24 May 2008 14:47:43 +0200] rev 26980
ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip