src/HOL/IMP/ROOT.ML

--- a/src/HOL/IMP/ROOT.ML	Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Thu Sep 15 09:44:08 2011 +0200
@@ -1,4 +1,7 @@
-no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs"];
+no_document use_thys
+  ["~~/src/HOL/ex/Interpretation_with_Defs",
+   "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
+  ];
 
 use_thys
 ["BExp",
@@ -12,7 +15,7 @@
  "Def_Ass_Sound_Big",
  "Def_Ass_Sound_Small",
  "Live",
- "AbsInt1_ivl",
+ "AbsInt2",
  "Hoare_Examples",
  "VC",
  "HoareT",