--- a/src/HOL/ex/ROOT.ML Tue Sep 20 13:56:01 2005 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Sep 20 13:56:34 2005 +0200
@@ -52,3 +52,4 @@
time_use_thy "Adder";
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
+HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";