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>