author | traytel |
Mon, 24 Oct 2016 16:53:32 +0200 | |
changeset 64378 | e9eb0b99a44c |
parent 64318 | 1e92b5c35615 |
child 66276 | acc3b7dd0b21 |
permissions | -rw-r--r-- |
32479 | 1 |
|
60526 | 2 |
section \<open>Comprehensive number theory\<close> |
32479 | 3 |
|
4 |
theory Number_Theory |
|
64318
1e92b5c35615
Repaired LaTeX in HOL-Data_Structures
eberlm <eberlm@in.tum.de>
parents:
64282
diff
changeset
|
5 |
imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington |
32479 | 6 |
begin |
7 |
||
8 |
end |
|
51173 | 9 |