author | haftmann |
Tue, 01 Sep 2009 15:39:33 +0200 | |
changeset 32479 | 521cc9bf2958 |
parent 24104 | src/HOL/NumberTheory/ROOT.ML@719fbe4fb77f |
child 41413 | 64cd30d6b0b8 |
permissions | -rw-r--r-- |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
1 |
|
32479 | 2 |
no_document use_thys ["Infinite_Set", "Permutation"]; |
24104 | 3 |
use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss", |
32479 | 4 |
"WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"]; |