src/HOL/Number_Theory/Number_Theory.thy
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