identical to timer (see timer), except that real times (i.e.,
wall-clock) times are reported, instead of CPU times. This can be
trusted on all operating systems (including Windows95/98).
User manual for Singular version 2-0-4, October 2002,
generated by texi2html.