src/HOL/Library/Quotient.thy
changeset 10681 ec76e17f73c5
parent 10551 ec9fab41b3a0
child 11099 b301d1f72552
equal deleted inserted replaced
10680:26e4aecf3207 10681:ec76e17f73c5
     1 (*  Title:      HOL/Library/Quotient.thy
     1 (*  Title:      HOL/Library/Quotient.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
       
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4 *)
     5 *)
     5 
     6 
     6 header {*
     7 header {*
     7   \title{Quotient types}
     8   \title{Quotient types}
     8   \author{Markus Wenzel}
     9   \author{Markus Wenzel}