author | eberlm <eberlm@in.tum.de> |
Tue, 16 Aug 2016 12:41:43 +0200 | |
changeset 63705 | 7d371a18b6a2 |
parent 63704 | 6209c06d776f |
child 63706 | 76c2f833abf4 |
--- 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