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