HTML.with_charset;

--- a/NEWS	Sat Sep 17 17:35:26 2005 +0200
+++ b/NEWS	Sat Sep 17 18:11:17 2005 +0200
@@ -918,6 +918,11 @@
 in porting non-Isar theories to Isar ones, while keeping ML proof
 scripts for the time being.
 
+* ML operator HTML.with_charset specifies the charset begin used for
+generated HTML files.  For example:
+
+  HTML.with_charset "utf-8" use_thy "Hebrew";
+
 
 *** System ***