changeset 41413 | 64cd30d6b0b8 |
parent 32479 | 521cc9bf2958 |
41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
---|---|
1 no_document use_thys [ |
|
2 "~~/src/HOL/Library/Infinite_Set", |
|
3 "~~/src/HOL/Library/Permutation" |
|
4 ]; |
|
1 |
5 |
2 no_document use_thys ["Infinite_Set", "Permutation"]; |
6 use_thys [ |
3 use_thys ["Fib", "Factorization", "Chinese", "WilsonRuss", |
7 "Fib", |
4 "WilsonBij", "Quadratic_Reciprocity", "Primes", "Pocklington"]; |
8 "Factorization", |
9 "Chinese", |
|
10 "WilsonRuss", |
|
11 "WilsonBij", |
|
12 "Quadratic_Reciprocity", |
|
13 "Primes", |
|
14 "Pocklington" |
|
15 ]; |