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";