Fri, 16 Aug 2013 22:39:31 +0200 more markup via Name_Space.check;
wenzelm [Fri, 16 Aug 2013 22:39:31 +0200] rev 53044
more markup via Name_Space.check; tuned signature;
Fri, 16 Aug 2013 21:33:36 +0200 more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
wenzelm [Fri, 16 Aug 2013 21:33:36 +0200] rev 53043
more standard attribute_setup / method_setup -- export key ML operations instead of parsers;
Fri, 16 Aug 2013 21:28:05 +0200 standardized aliases;
wenzelm [Fri, 16 Aug 2013 21:28:05 +0200] rev 53042
standardized aliases;
Fri, 16 Aug 2013 20:58:15 +0200 more markup -- avoid old Locale.extern;
wenzelm [Fri, 16 Aug 2013 20:58:15 +0200] rev 53041
more markup -- avoid old Locale.extern; removed obsolete Locale.intern -- prefer Locale.check;
Fri, 16 Aug 2013 19:03:31 +0200 renamed function
blanchet [Fri, 16 Aug 2013 19:03:31 +0200] rev 53040
renamed function
Fri, 16 Aug 2013 18:56:33 +0200 eliminate quasi-duplicate function
blanchet [Fri, 16 Aug 2013 18:56:33 +0200] rev 53039
eliminate quasi-duplicate function
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 tip