function timestamp() {
	document.write('<P><FONT SIZE=1>(This page was last modified on <B>'+
		document.lastModified+'</B>)</FONT></P>');
}