function display_links() {
    document.write("<center>")
    document.write("<a href=\"./index.html\">15-712 Home</a> | <a href=\"schedule.html\">Schedule and Lectures</a> | <a href=\"readings.html\">Reading List</a> | <a href=\"summaries.html\">Summaries</a> | <a href=\"projects.html\">Projects</a>")
    document.write("</center>")
}