diff -r 26e5b41faa74 -r 79696161ae16 CookBook/ROOT.ML --- a/CookBook/ROOT.ML Mon Feb 16 17:17:24 2009 +0000 +++ b/CookBook/ROOT.ML Tue Feb 17 02:12:19 2009 +0000 @@ -1,13 +1,13 @@ set quick_and_dirty; no_document use_thy "Base"; +no_document use_thy "Package/Simple_Inductive_Package"; use_thy "Intro"; use_thy "FirstSteps"; use_thy "Parsing"; use_thy "Tactical"; -no_document use_thy "Package/Simple_Inductive_Package"; use_thy "Package/Ind_Intro"; use_thy "Package/Ind_Examples"; use_thy "Package/Ind_General_Scheme";