Thu, 17 Apr 2008 16:30:50 +0200 token translations: context dependent, result Pretty.T;
wenzelm [Thu, 17 Apr 2008 16:30:50 +0200] rev 26704
token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;
Thu, 17 Apr 2008 16:30:48 +0200 removed obsolete raw_str;
wenzelm [Thu, 17 Apr 2008 16:30:48 +0200] rev 26703
removed obsolete raw_str; added mark;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip