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