changeset 65417 | fc41a5650fb1 |
parent 63830 | 2ea3725a34bd |
child 66258 | 2b83dd24b301 |
--- a/src/HOL/Proofs/Extraction/Euclid.thy Thu Apr 06 08:33:37 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Euclid.thy Thu Apr 06 21:37:13 2017 +0200 @@ -8,7 +8,7 @@ theory Euclid imports - "~~/src/HOL/Number_Theory/Primes" + "~~/src/HOL/Computational_Algebra/Primes" Util "~~/src/HOL/Library/Code_Target_Numeral" begin