| author | berghofe |
| Fri, 19 Apr 2002 14:51:33 +0200 | |
| changeset 13093 | ab0335307905 |
| parent 11368 | 9c1995c73383 |
| child 13871 | 26e5f5e624f6 |
| permissions | -rw-r--r-- |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
1 |
|
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
2 |
no_document use_thy "Permutation"; |
| 11368 | 3 |
no_document use_thy "Primes"; |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
|
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
5 |
use_thy "Fib"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
6 |
use_thy "Factorization"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
7 |
use_thy "Chinese"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
8 |
use_thy "EulerFermat"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
9 |
use_thy "WilsonRuss"; |
|
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
10 |
use_thy "WilsonBij"; |