Mon, 22 May 2006 22:29:15 +0200 wenzelm specifications_of: lhs/rhs represented as typargs;
Mon, 22 May 2006 21:27:01 +0200 wenzelm export raw_unifys, could_unifys;
Sat, 20 May 2006 23:45:37 +0200 wenzelm made smlnj happy;
Sat, 20 May 2006 23:37:04 +0200 wenzelm export raw_matches;
Sat, 20 May 2006 23:37:03 +0200 wenzelm tuned Defs interfaces;
Sat, 20 May 2006 23:37:02 +0200 wenzelm yet another re-implementation:
Sat, 20 May 2006 23:37:02 +0200 wenzelm removed obsolete partition (cf. List.partition);
(0) -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip