| changeset 69804 | 9efccbad7d42 |
| parent 67306 | 897344e33c26 |
| child 72622 | 830222403681 |
--- a/src/Pure/Thy/html.ML Wed Feb 13 11:25:23 2019 +0100 +++ b/src/Pure/Thy/html.ML Thu Feb 14 14:44:41 2019 +0100 @@ -126,7 +126,7 @@ (* document *) fun begin_document symbols title = - "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^ + XML.header ^ "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^ "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^ "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^