| changeset 64318 | 1e92b5c35615 |
| parent 64282 | 261d42f0bfac |
| child 66276 | acc3b7dd0b21 |
--- a/src/HOL/Number_Theory/Number_Theory.thy Thu Oct 20 13:53:36 2016 +0200 +++ b/src/HOL/Number_Theory/Number_Theory.thy Thu Oct 20 17:28:09 2016 +0200 @@ -2,7 +2,7 @@ section \<open>Comprehensive number theory\<close> theory Number_Theory -imports Fib Residues Eratosthenes QuadraticReciprocity Pocklington +imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington begin end