diff -r 48d935524988 -r c5d0fdc260fa src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Mon Apr 11 15:07:15 2016 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Mon Apr 11 15:26:58 2016 +0200 @@ -5,7 +5,7 @@ section \Quotient infrastructure for the set type\ theory Quotient_Set -imports Main Quotient_Syntax +imports Quotient_Syntax begin subsection \Contravariant set map (vimage) and set relator, rules for the Quotient package\