src/HOL/ex/ROOT.ML

--- a/src/HOL/ex/ROOT.ML	Tue Jun 02 16:23:43 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue Jun 02 18:26:01 2009 +0200
@@ -6,7 +6,6 @@
 no_document use_thys [
   "State_Monad",
   "Efficient_Nat_examples",
-  "ExecutableContent",
   "FuncSet",
   "Word",
   "Eval_Examples",
@@ -67,7 +66,8 @@
   "HarmonicSeries",
   "Refute_Examples",
   "Quickcheck_Examples",
-  "Formal_Power_Series_Examples"
+  "Formal_Power_Series_Examples",
+  "Landau"
 ];
 
 setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";