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