changeset 14981 | e73f8140af78 |
parent 13871 | 26e5f5e624f6 |
child 15392 | 290bc97038c7 |
14980:267cc670317a | 14981:e73f8140af78 |
---|---|
1 (* Title: HOL/Quadratic_Reciprocity/Residues.thy |
1 (* Title: HOL/Quadratic_Reciprocity/Residues.thy |
2 ID: $Id$ |
|
2 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 Authors: Jeremy Avigad, David Gray, and Adam Kramer |
3 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4 *) |
4 *) |
5 |
5 |
6 header {* Residue Sets *} |
6 header {* Residue Sets *} |
7 |
7 |
8 theory Residues = Int2:; |
8 theory Residues = Int2:; |