Use $decimal in timestamp.exp

This patch fixes a review comment by Tom de Vries.  He pointed out
that the new timestamp.exp should use the $decimal convenience regexp.