| changeset 32479 | 521cc9bf2958 |
| parent 24104 | 719fbe4fb77f |
| child 41413 | 64cd30d6b0b8 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Old_Number_Theory/ROOT.ML Tue Sep 01 15:39:33 2009 +0200 @@ -0,0 +1,4 @@ + +no_document use_thys ["Infinite_Set", "Permutation"]; +use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss", + "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"];