author | wenzelm |
Wed, 17 May 2006 01:23:43 +0200 | |
changeset 19671 | e293e16d1442 |
parent 14271 | 8ed6989228bb |
child 20809 | 6c4fd0b4b63a |
permissions | -rw-r--r-- |
19671 | 1 |
(* $Id$ *) |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
2 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
3 |
no_document use_thy "Permutation"; |
11368 | 4 |
no_document use_thy "Primes"; |
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
11049
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
6 |
use_thy "Fib"; |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
7 |
use_thy "Factorization"; |
7eef34adb852
HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents:
9944
diff
changeset
|
8 |
use_thy "Chinese"; |
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"; |
13871
26e5f5e624f6
Gauss's law of quadratic reciprocity by Avigad, Gray and Kramer
paulson
parents:
11368
diff
changeset
|
11 |
use_thy "Quadratic_Reciprocity"; |