| changeset 62954 | c5d0fdc260fa |
| parent 60500 | 903bb1495239 |
| child 67399 | eab6ce8368fa |
--- 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 \<open>Quotient infrastructure for the set type\<close> theory Quotient_Set -imports Main Quotient_Syntax +imports Quotient_Syntax begin subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>