--- a/src/HOL/ex/ROOT.ML Thu May 17 21:51:32 2007 +0200
+++ b/src/HOL/ex/ROOT.ML Thu May 17 22:33:41 2007 +0200
@@ -79,3 +79,5 @@
HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";
HTML.with_charset "utf-8" (no_document time_use_thy) "Chinese";
+
+time_use_thy "Unification";