function writeNav3(which) {
document.write("<TABLE align=center border='0' cellpadding='10' bgcolor='#000000' nosave='' >"+ 
"<TR><FONT +=5><TD bgcolor=");
writeCol3(1,which);
document.write("><A HREF=./index.html>Papers</A></TD><TD bgcolor=");
writeCol3(2,which);
document.write("><A HREF=./tech.html>Technical Reports</A></TD><TD bgcolor=");
writeCol3(3,which);
document.write("><A HREF=./prep.html>In preparation</A></TD><TD bgcolor=");
writeCol3(4,which);
document.write("><A HREF=./thesis.html>Thesis</A></TD><TD bgcolor=");
writeCol3(5,which);
document.write("><A HREF=./talks.html>Talks and Posters</A></TD></TR></TABLE>");
}

function writeCol3(here,which) {
 if (which == here)
	document.write("#55AA55");
 else	
	document.write("#BBBBBB");
}