src/HOL/Number_Theory/Number_Theory.thy
changeset 69785 9e326f6f8a24
parent 66276 acc3b7dd0b21
child 69790 154cf64e403e
     1.1 --- a/src/HOL/Number_Theory/Number_Theory.thy	Sat Feb 02 15:52:14 2019 +0100
     1.2 +++ b/src/HOL/Number_Theory/Number_Theory.thy	Mon Feb 04 12:16:03 2019 +0100
     1.3 @@ -2,7 +2,14 @@
     1.4  section \<open>Comprehensive number theory\<close>
     1.5  
     1.6  theory Number_Theory
     1.7 -imports Fib Residues Eratosthenes Quadratic_Reciprocity Pocklington Prime_Powers
     1.8 +imports
     1.9 +  Fib
    1.10 +  Residues
    1.11 +  Eratosthenes
    1.12 +  Quadratic_Reciprocity
    1.13 +  Pocklington
    1.14 +  Prime_Powers
    1.15 +  Residue_Primitive_Roots
    1.16  begin
    1.17  
    1.18  end