src/HOL/Library/Quotient_Product.thy
changeset 62954 c5d0fdc260fa
parent 61424 c3658c18b7bc
child 67399 eab6ce8368fa
--- a/src/HOL/Library/Quotient_Product.thy	Mon Apr 11 15:07:15 2016 +0200
+++ b/src/HOL/Library/Quotient_Product.thy	Mon Apr 11 15:26:58 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Quotient infrastructure for the product type\<close>
 
 theory Quotient_Product
-imports Main Quotient_Syntax
+imports Quotient_Syntax
 begin
 
 subsection \<open>Rules for the Quotient package\<close>