src/HOL/Library/Normalized_Fraction.thy
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