| author | wenzelm |
| Mon, 23 Oct 2000 22:17:55 +0200 | |
| changeset 10313 | 51e830bb7abe |
| parent 9944 | 2a705d1af4dc |
| child 11049 | 7eef34adb852 |
| permissions | -rw-r--r-- |
|
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/NumberTheory/ROOT |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
4 |
Copyright 2000 University of Cambridge |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
5 |
|
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
6 |
Number theory developments by Thomas M Rasmussen |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
7 |
*) |
|
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset
|
8 |
|
| 9944 | 9 |
time_use_thy "Primes"; |
10 |
time_use_thy "Fib"; |
|
11 |
with_path "../Induct" time_use_thy "Factorization"; |
|
12 |
time_use_thy "Chinese"; |
|
13 |
time_use_thy "EulerFermat"; |
|
14 |
time_use_thy "WilsonRuss"; |
|
15 |
time_use_thy "WilsonBij"; |