--- a/src/HOL/Library/Quotient_Product.thy Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Sun Mar 14 14:31:24 2010 +0100
@@ -1,12 +1,13 @@
-(* Title: Quotient_Product.thy
+(* Title: HOL/Library/Quotient_Product.thy
Author: Cezary Kaliszyk and Christian Urban
*)
+
+header {* Quotient infrastructure for the product type *}
+
theory Quotient_Product
imports Main Quotient_Syntax
begin
-section {* Quotient infrastructure for the product type. *}
-
fun
prod_rel
where
@@ -100,5 +101,4 @@
shows "prod_rel (op =) (op =) = (op =)"
by (simp add: expand_fun_eq)
-
end