src/HOL/Library/Quotient_Sum.thy
changeset 35788 f1deaca15ca3
parent 35243 024fef37a65d
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:29:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:31:24 2010 +0100
     1.3 @@ -1,12 +1,13 @@
     1.4 -(*  Title:      Quotient_Sum.thy
     1.5 +(*  Title:      HOL/Library/Quotient_Sum.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8 +
     1.9 +header {* Quotient infrastructure for the sum type *}
    1.10 +
    1.11  theory Quotient_Sum
    1.12  imports Main Quotient_Syntax
    1.13  begin
    1.14  
    1.15 -section {* Quotient infrastructure for the sum type. *}
    1.16 -
    1.17  fun
    1.18    sum_rel
    1.19  where