Time functions

[HMS Surprise]

I wish to generate a datetime string that has the following format.
'05/02/2007 12:46'. The leading zeros are required.

I found '14.2 time' in the library reference and have pulled in
localtime. Are there any formatting functions available or do I need
to make my own? Perhaps there is something similar to C's printf
formatting.

Thanks,

jvh (whose newbieism is most glaring)