changeset 65366 | 10ca63a18e56 |
parent 64592 | 7759f1766189 |
--- a/src/HOL/Library/Normalized_Fraction.thy Mon Apr 03 23:31:31 2017 +0200 +++ b/src/HOL/Library/Normalized_Fraction.thy Tue Apr 04 11:52:28 2017 +0200 @@ -6,7 +6,7 @@ imports Main "~~/src/HOL/Number_Theory/Euclidean_Algorithm" - "~~/src/HOL/Library/Fraction_Field" + Fraction_Field begin definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where