# HG changeset patch
# User wenzelm
# Date 1268573484 -3600
# Node ID f1deaca15ca36e67788339706554b2313083f908
# Parent  afdf1c4958b2b189a0f520bf896eda5b3cf748e9
observe standard header format;

diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Sun Mar 14 14:31:24 2010 +0100
@@ -1,12 +1,13 @@
-(*  Title:      Quotient_List.thy
+(*  Title:      HOL/Library/Quotient_List.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
+
+header {* Quotient infrastructure for the list type *}
+
 theory Quotient_List
 imports Main Quotient_Syntax
 begin
 
-section {* Quotient infrastructure for the list type. *}
-
 fun
   list_rel
 where
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:31:24 2010 +0100
@@ -1,12 +1,13 @@
-(*  Title:      Quotient_Option.thy
+(*  Title:      HOL/Library/Quotient_Option.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
+
+header {* Quotient infrastructure for the option type *}
+
 theory Quotient_Option
 imports Main Quotient_Syntax
 begin
 
-section {* Quotient infrastructure for the option type. *}
-
 fun
   option_rel
 where
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Library/Quotient_Product.thy
--- 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
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Library/Quotient_Sum.thy
--- a/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:31:24 2010 +0100
@@ -1,12 +1,13 @@
-(*  Title:      Quotient_Sum.thy
+(*  Title:      HOL/Library/Quotient_Sum.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
+
+header {* Quotient infrastructure for the sum type *}
+
 theory Quotient_Sum
 imports Main Quotient_Syntax
 begin
 
-section {* Quotient infrastructure for the sum type. *}
-
 fun
   sum_rel
 where
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Mar 14 14:31:24 2010 +0100
@@ -1,8 +1,7 @@
-(*  Title:      quotient_def.thy
+(*  Title:      HOL/Tools/Quotient/quotient_def.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Definitions for constants on quotient types.
-
+Definitions for constants on quotient types.
 *)
 
 signature QUOTIENT_DEF =
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sun Mar 14 14:31:24 2010 +0100
@@ -1,11 +1,9 @@
-(*  Title:      quotient_info.thy
+(*  Title:      HOL/Tools/Quotient/quotient_info.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Data slots for the quotient package.
-
+Data slots for the quotient package.
 *)
 
-
 signature QUOTIENT_INFO =
 sig
   exception NotFound
@@ -290,4 +288,3 @@
 
 
 end; (* structure *)
-
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 14 14:31:24 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_tacs.thy
+(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Tactics for solving goal arising from lifting
-    theorems to quotient types.
+Tactics for solving goal arising from lifting theorems to quotient
+types.
 *)
 
 signature QUOTIENT_TACS =
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:31:24 2010 +0100
@@ -1,8 +1,8 @@
-(*  Title:      quotient_term.thy
+(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Constructs terms corresponding to goals from
-    lifting theorems to quotient types.
+Constructs terms corresponding to goals from lifting theorems to
+quotient types.
 *)
 
 signature QUOTIENT_TERM =
@@ -779,8 +779,4 @@
   lift_aux t
 end
 
-
 end; (* structure *)
-
-
-
diff -r afdf1c4958b2 -r f1deaca15ca3 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 14:29:30 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 14:31:24 2010 +0100
@@ -1,8 +1,7 @@
-(*  Title:      quotient_typ.thy
+(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-    Definition of a quotient type.
-
+Definition of a quotient type.
 *)
 
 signature QUOTIENT_TYPE =