src/HOL/Computational_Algebra/Primes.thy
changeset 66453 cc19f7ca2ed6
parent 65583 8d53b3bebab4
child 66837 6ba663ff2b1c
     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 13:55:05 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Aug 18 20:47:47 2017 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  section \<open>Primes\<close>
     1.5  
     1.6  theory Primes
     1.7 -imports "~~/src/HOL/Binomial" Euclidean_Algorithm
     1.8 +imports HOL.Binomial Euclidean_Algorithm
     1.9  begin
    1.10  
    1.11  (* As a simp or intro rule,