diff -r d94755882e36 -r 94538ddcac9b ProgTutorial/ROOT.ML --- a/ProgTutorial/ROOT.ML Thu May 27 10:39:07 2010 +0200 +++ b/ProgTutorial/ROOT.ML Sat May 29 12:30:02 2010 +0200 @@ -2,6 +2,8 @@ no_document use_thy "Base"; no_document use_thy "Package/Simple_Inductive_Package"; +no_document use_thy "~~/src/HOL/Number_Theory/Primes"; +no_document use_thy "Efficient_Nat"; use_thy "Intro"; use_thy "FirstSteps"; @@ -23,6 +25,7 @@ use_thy "Recipes/Antiquotes"; use_thy "Recipes/TimeLimit"; use_thy "Recipes/Timing"; +use_thy "Recipes/CallML"; use_thy "Recipes/ExternalSolver"; use_thy "Recipes/Oracle"; use_thy "Recipes/Sat";