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 ***)