author | wenzelm |
Mon, 13 May 2002 11:05:27 +0200 | |
changeset 13142 | 1ebd8ed5a1a0 |
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"; |