
diff -r 029e6247210e -r 1e92b5c35615 src/HOL/Number_Theory/Number_Theory.thy
--- 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




