--- 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
--- 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
--- 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
--- 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
--- 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 =
--- 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 *)
-
--- 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 =
--- 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 *)
-
-
-
--- 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 =