Thu, 14 Sep 2006 00:23:02 +0200 made SML/NJ happy;
wenzelm [Thu, 14 Sep 2006 00:23:02 +0200] rev 20532
made SML/NJ happy;
Wed, 13 Sep 2006 21:41:31 +0200 added exists_type;
wenzelm [Wed, 13 Sep 2006 21:41:31 +0200] rev 20531
added exists_type;
Wed, 13 Sep 2006 21:41:25 +0200 renamed NameSpace.drop_base to NameSpace.qualifier;
wenzelm [Wed, 13 Sep 2006 21:41:25 +0200] rev 20530
renamed NameSpace.drop_base to NameSpace.qualifier;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip