changeset 14083 | aed5d25c4a0c |
parent 13531 | 5825aef91ac5 |
child 14534 | 7a46bdcd92f2 |
--- a/src/Pure/Thy/html.ML Sun Jun 29 21:29:15 2003 +0200 +++ b/src/Pure/Thy/html.ML Mon Jun 30 12:23:00 2003 +0200 @@ -164,8 +164,11 @@ (* document *) fun begin_document title = - "<html>\n\ + "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \"http://www.w3.org/TR/html4/loose.dtd\">\n\ + \\n\ + \<html>\n\ \<head>\n\ + \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=iso-8859-1\">\n\ \<title>" ^ plain (title ^ " (" ^ version ^ ")") ^ "</title>\n\ \</head>\n\ \\n\