| changeset 17457 | 5b9538fc6d67 |
| parent 17445 | 3c9c46b820f5 |
| child 17495 | ddb14cbec6a2 |
--- 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 ***