Wed, 03 Mar 2010 00:33:33 +0100 removed unused external_names;
wenzelm [Wed, 03 Mar 2010 00:33:33 +0100] rev 35432
removed unused external_names;
Wed, 03 Mar 2010 00:33:02 +0100 cleanup type translations;
wenzelm [Wed, 03 Mar 2010 00:33:02 +0100] rev 35431
cleanup type translations;
Wed, 03 Mar 2010 00:32:14 +0100 adapted to authentic syntax -- actual types are verbatim;
wenzelm [Wed, 03 Mar 2010 00:32:14 +0100] rev 35430
adapted to authentic syntax -- actual types are verbatim;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip