changeset 63500 | 0dac030afd36 |
parent 63499 | 9c9a59949887 |
child 63539 | 70d4d9e5707b |
--- a/src/HOL/Number_Theory/Polynomial_Factorial.thy Thu Jul 14 14:43:09 2016 +0200 +++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy Thu Jul 14 14:49:09 2016 +0200 @@ -2,9 +2,8 @@ imports Complex_Main Euclidean_Algorithm - "~~/src/HOL/Library/Fraction_Field" "~~/src/HOL/Library/Polynomial" - "/home/manuel/hg/Linear_Recurrences/Normalized_Fraction" + "~~/src/HOL/Library/Normalized_Fraction" begin subsection \<open>Prelude\<close>