src/HOL/ROOT
changeset 55159 608c157d743d
parent 55123 a389b50e6a42
child 55240 efc4c0e0e14a
--- a/src/HOL/ROOT	Mon Jan 27 17:13:33 2014 +0000
+++ b/src/HOL/ROOT	Wed Jan 29 12:51:37 2014 +0000
@@ -258,8 +258,8 @@
   theories [document = false]
     (* Preliminaries from set and number theory *)
     "~~/src/HOL/Library/FuncSet"
-    "~~/src/HOL/Old_Number_Theory/Primes"
-    "~~/src/HOL/Library/Binomial"
+    "~~/src/HOL/Number_Theory/Primes"
+    "~~/src/HOL/Number_Theory/Binomial"
     "~~/src/HOL/Library/Permutation"
   theories
     (*** New development, based on explicit structures ***)