src/HOL/Library/Quotient_Product.thy
changeset 35788 f1deaca15ca3
parent 35222 4f1fba00f66d
child 36695 b434506fb0d4
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Sun Mar 14 14:29:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Sun Mar 14 14:31:24 2010 +0100
     1.3 @@ -1,12 +1,13 @@
     1.4 -(*  Title:      Quotient_Product.thy
     1.5 +(*  Title:      HOL/Library/Quotient_Product.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8 +
     1.9 +header {* Quotient infrastructure for the product type *}
    1.10 +
    1.11  theory Quotient_Product
    1.12  imports Main Quotient_Syntax
    1.13  begin
    1.14  
    1.15 -section {* Quotient infrastructure for the product type. *}
    1.16 -
    1.17  fun
    1.18    prod_rel
    1.19  where
    1.20 @@ -100,5 +101,4 @@
    1.21    shows "prod_rel (op =) (op =) = (op =)"
    1.22    by (simp add: expand_fun_eq)
    1.23  
    1.24 -
    1.25  end