../ decimal.dtx 06-Jun-2011 03:45 14683 decimal.ins 06-Jun-2011 03:45 1577 decimal.pdf 06-Jun-2011 03:45 187033