1.1 --- a/src/HOL/ex/ROOT.ML Fri Dec 03 20:38:58 2010 +0100
1.2 +++ b/src/HOL/ex/ROOT.ML Fri Dec 03 21:30:41 2010 +0100
1.3 @@ -8,7 +8,10 @@
1.4 "Efficient_Nat_examples",
1.5 "FuncSet",
1.6 "Eval_Examples",
1.7 - "Normalization_by_Evaluation"
1.8 + "Normalization_by_Evaluation",
1.9 + "Hebrew",
1.10 + "Chinese",
1.11 + "Serbian"
1.12 ];
1.13
1.14 use_thys [
1.15 @@ -71,9 +74,6 @@
1.16 "Birthday_Paradoxon"
1.17 ];
1.18
1.19 -HTML.with_charset "utf-8" (no_document use_thys)
1.20 - ["Hebrew", "Chinese", "Serbian"];
1.21 -
1.22 use_thy "SVC_Oracle";
1.23 if getenv "SVC_HOME" = "" then ()
1.24 else use_thy "svc_test";