# HG changeset patch
# User wenzelm
# Date 1126973477 -7200
# Node ID 5b9538fc6d679982b605fcc78e2d1985cd4acced
# Parent  bcf7544875b26f4712686157182094daa11e9471
HTML.with_charset;

diff -r bcf7544875b2 -r 5b9538fc6d67 NEWS
--- 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 ***