# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1471344103 -7200
# Node ID 7d371a18b6a2f792d53c83885bac58b8e128c019
# Parent  6209c06d776fa8e2c98925b2b28abe9ca64b1ddf
Polynomial algebra cleanup (tuned)

diff -r 6209c06d776f -r 7d371a18b6a2 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