src/HOL/Number_Theory/Primes.thy
changeset 59667 651ea265d568
parent 58954 18750e86d5b8
child 59669 de7792ea4090
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 11:56:32 2015 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 15:20:40 2015 +0000
     1.3 @@ -28,7 +28,7 @@
     1.4  section {* Primes *}
     1.5  
     1.6  theory Primes
     1.7 -imports "~~/src/HOL/GCD"
     1.8 +imports "~~/src/HOL/GCD" "~~/src/HOL/Fact"
     1.9  begin
    1.10  
    1.11  declare [[coercion int]]