ProgTutorial/ROOT.ML
changeset 459 4532577b61e0
parent 441 520127b708e6
child 525 92a3600e50e4
--- a/ProgTutorial/ROOT.ML	Wed Feb 23 23:55:37 2011 +0000
+++ b/ProgTutorial/ROOT.ML	Fri Mar 18 02:53:14 2011 +0100
@@ -3,7 +3,7 @@
 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";
+no_document use_thy "~~/src/HOL/Library/Efficient_Nat";
 
 use_thy "Intro";
 use_thy "First_Steps";