--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jul 18 20:51:22 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Wed Jul 18 20:51:23 2018 +0200
@@ -7,7 +7,7 @@
*)
theory Quotient_Int
-imports "HOL-Library.Quotient_Product" HOL.Nat
+imports "HOL-Library.Quotient_Product"
begin
fun