Polynomial algebra cleanup (tuned)
authoreberlm <eberlm@in.tum.de>
Tue, 16 Aug 2016 12:41:43 +0200
changeset 63705 7d371a18b6a2
parent 63704 6209c06d776f
child 63706 76c2f833abf4
Polynomial algebra cleanup (tuned)
src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Tue Aug 16 12:02:09 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Tue Aug 16 12:41:43 2016 +0200
@@ -1,7 +1,7 @@
 theory Polynomial_Factorial
 imports 
   Complex_Main
-  Euclidean_Algorithm 
+  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
   "~~/src/HOL/Library/Polynomial"
   "~~/src/HOL/Library/Normalized_Fraction"
 begin