src/HOL/ex/ROOT.ML
changeset 41194 3f697c636fa1
parent 40880 dc55e6752046
child 41661 64cd30d6b0b8
     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";