src/HOL/Library/Quotient_Sum.thy
changeset 58881 b9556a055632
parent 55943 5c2df04e97d1
child 58916 229765cc3414
equal deleted inserted replaced
58880:0baae4311a9f 58881:b9556a055632
     1 (*  Title:      HOL/Library/Quotient_Sum.thy
     1 (*  Title:      HOL/Library/Quotient_Sum.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     3 *)
     4 
     4 
     5 header {* Quotient infrastructure for the sum type *}
     5 section {* Quotient infrastructure for the sum type *}
     6 
     6 
     7 theory Quotient_Sum
     7 theory Quotient_Sum
     8 imports Main Quotient_Syntax
     8 imports Main Quotient_Syntax
     9 begin
     9 begin
    10 
    10