
diff -r db0c70767d86 -r 4ce18f389f53 src/HOL/Quotient_Examples/Quotient_Int.thy
--- 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




