CookBook/ROOT.ML
changeset 122 79696161ae16
parent 120 c39f83d8daeb
child 127 74846cb0fff9
--- 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";