# HG changeset patch
# User wenzelm
# Date 1126973486 -7200
# Node ID 92d36be64b46d5ce06f6a64ec8daec3d1bb7b10d
# Parent  93fc1211603f314798dedb16be6fd2b563bf39a6
Hebrew: HTML.with_charset;

diff -r 93fc1211603f -r 92d36be64b46 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sat Sep 17 18:11:25 2005 +0200
+++ b/src/HOL/ex/ROOT.ML	Sat Sep 17 18:11:26 2005 +0200
@@ -51,4 +51,4 @@
 no_document use_thy "Word";
 time_use_thy "Adder";
 
-no_document time_use_thy "Hebrew";
+HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";