Wed, 30 Sep 2009 15:00:43 +0200 wenzelm report unreferenced ids;
Wed, 30 Sep 2009 11:45:42 +0200 wenzelm tuned whitespace;
Wed, 30 Sep 2009 11:36:12 +0200 wenzelm more uniform treatment of structure Unsynchronized in ML bootstrap phase;
Wed, 30 Sep 2009 09:25:18 +0200 haftmann merged
Wed, 30 Sep 2009 08:28:23 +0200 haftmann mandatory prefix where appropriate
Wed, 30 Sep 2009 08:22:07 +0200 haftmann mandatory prefix where appropriate
Wed, 30 Sep 2009 08:21:53 +0200 haftmann tuned whitespace
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip