src/HOL/ex/ROOT.ML
changeset 17466 92d36be64b46
parent 17413 89ccb3799428
child 17505 928bd7053d6a
     1.1 --- a/src/HOL/ex/ROOT.ML	Sat Sep 17 18:11:25 2005 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Sat Sep 17 18:11:26 2005 +0200
     1.3 @@ -51,4 +51,4 @@
     1.4  no_document use_thy "Word";
     1.5  time_use_thy "Adder";
     1.6  
     1.7 -no_document time_use_thy "Hebrew";
     1.8 +HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew";