Tue, 16 Oct 2007 17:06:20 +0200 tuned Const.the_abbreviation;
wenzelm [Tue, 16 Oct 2007 17:06:20 +0200] rev 25054
tuned Const.the_abbreviation;
Tue, 16 Oct 2007 17:06:19 +0200 misc cleanup of abbrev/local_const;
wenzelm [Tue, 16 Oct 2007 17:06:19 +0200] rev 25053
misc cleanup of abbrev/local_const;
Tue, 16 Oct 2007 17:06:18 +0200 added revert_abbrev;
wenzelm [Tue, 16 Oct 2007 17:06:18 +0200] rev 25052
added revert_abbrev; contract_abbrevs: ignore Syntax.internalM (changed meaning of this special case); print_abbrevs: proper treatment of global consts (after local/global swap);
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip