observe standard header format;
authorwenzelm
Sun Mar 14 14:31:24 2010 +0100 (2010-03-14)
changeset 35788f1deaca15ca3
parent 35787 afdf1c4958b2
child 35789 a2b163256f9b
observe standard header format;
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Library/Quotient_List.thy	Sun Mar 14 14:29:30 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_List.thy	Sun Mar 14 14:31:24 2010 +0100
     1.3 @@ -1,12 +1,13 @@
     1.4 -(*  Title:      Quotient_List.thy
     1.5 +(*  Title:      HOL/Library/Quotient_List.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8 +
     1.9 +header {* Quotient infrastructure for the list type *}
    1.10 +
    1.11  theory Quotient_List
    1.12  imports Main Quotient_Syntax
    1.13  begin
    1.14  
    1.15 -section {* Quotient infrastructure for the list type. *}
    1.16 -
    1.17  fun
    1.18    list_rel
    1.19  where
     2.1 --- a/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:29:30 2010 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Option.thy	Sun Mar 14 14:31:24 2010 +0100
     2.3 @@ -1,12 +1,13 @@
     2.4 -(*  Title:      Quotient_Option.thy
     2.5 +(*  Title:      HOL/Library/Quotient_Option.thy
     2.6      Author:     Cezary Kaliszyk and Christian Urban
     2.7  *)
     2.8 +
     2.9 +header {* Quotient infrastructure for the option type *}
    2.10 +
    2.11  theory Quotient_Option
    2.12  imports Main Quotient_Syntax
    2.13  begin
    2.14  
    2.15 -section {* Quotient infrastructure for the option type. *}
    2.16 -
    2.17  fun
    2.18    option_rel
    2.19  where
     3.1 --- a/src/HOL/Library/Quotient_Product.thy	Sun Mar 14 14:29:30 2010 +0100
     3.2 +++ b/src/HOL/Library/Quotient_Product.thy	Sun Mar 14 14:31:24 2010 +0100
     3.3 @@ -1,12 +1,13 @@
     3.4 -(*  Title:      Quotient_Product.thy
     3.5 +(*  Title:      HOL/Library/Quotient_Product.thy
     3.6      Author:     Cezary Kaliszyk and Christian Urban
     3.7  *)
     3.8 +
     3.9 +header {* Quotient infrastructure for the product type *}
    3.10 +
    3.11  theory Quotient_Product
    3.12  imports Main Quotient_Syntax
    3.13  begin
    3.14  
    3.15 -section {* Quotient infrastructure for the product type. *}
    3.16 -
    3.17  fun
    3.18    prod_rel
    3.19  where
    3.20 @@ -100,5 +101,4 @@
    3.21    shows "prod_rel (op =) (op =) = (op =)"
    3.22    by (simp add: expand_fun_eq)
    3.23  
    3.24 -
    3.25  end
     4.1 --- a/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:29:30 2010 +0100
     4.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Sun Mar 14 14:31:24 2010 +0100
     4.3 @@ -1,12 +1,13 @@
     4.4 -(*  Title:      Quotient_Sum.thy
     4.5 +(*  Title:      HOL/Library/Quotient_Sum.thy
     4.6      Author:     Cezary Kaliszyk and Christian Urban
     4.7  *)
     4.8 +
     4.9 +header {* Quotient infrastructure for the sum type *}
    4.10 +
    4.11  theory Quotient_Sum
    4.12  imports Main Quotient_Syntax
    4.13  begin
    4.14  
    4.15 -section {* Quotient infrastructure for the sum type. *}
    4.16 -
    4.17  fun
    4.18    sum_rel
    4.19  where
     5.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Mar 14 14:29:30 2010 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Mar 14 14:31:24 2010 +0100
     5.3 @@ -1,8 +1,7 @@
     5.4 -(*  Title:      quotient_def.thy
     5.5 +(*  Title:      HOL/Tools/Quotient/quotient_def.thy
     5.6      Author:     Cezary Kaliszyk and Christian Urban
     5.7  
     5.8 -    Definitions for constants on quotient types.
     5.9 -
    5.10 +Definitions for constants on quotient types.
    5.11  *)
    5.12  
    5.13  signature QUOTIENT_DEF =
     6.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Sun Mar 14 14:29:30 2010 +0100
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sun Mar 14 14:31:24 2010 +0100
     6.3 @@ -1,11 +1,9 @@
     6.4 -(*  Title:      quotient_info.thy
     6.5 +(*  Title:      HOL/Tools/Quotient/quotient_info.thy
     6.6      Author:     Cezary Kaliszyk and Christian Urban
     6.7  
     6.8 -    Data slots for the quotient package.
     6.9 -
    6.10 +Data slots for the quotient package.
    6.11  *)
    6.12  
    6.13 -
    6.14  signature QUOTIENT_INFO =
    6.15  sig
    6.16    exception NotFound
    6.17 @@ -290,4 +288,3 @@
    6.18  
    6.19  
    6.20  end; (* structure *)
    6.21 -
     7.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 14 14:29:30 2010 +0100
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 14 14:31:24 2010 +0100
     7.3 @@ -1,8 +1,8 @@
     7.4 -(*  Title:      quotient_tacs.thy
     7.5 +(*  Title:      HOL/Tools/Quotient/quotient_tacs.thy
     7.6      Author:     Cezary Kaliszyk and Christian Urban
     7.7  
     7.8 -    Tactics for solving goal arising from lifting
     7.9 -    theorems to quotient types.
    7.10 +Tactics for solving goal arising from lifting theorems to quotient
    7.11 +types.
    7.12  *)
    7.13  
    7.14  signature QUOTIENT_TACS =
     8.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:29:30 2010 +0100
     8.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sun Mar 14 14:31:24 2010 +0100
     8.3 @@ -1,8 +1,8 @@
     8.4 -(*  Title:      quotient_term.thy
     8.5 +(*  Title:      HOL/Tools/Quotient/quotient_term.thy
     8.6      Author:     Cezary Kaliszyk and Christian Urban
     8.7  
     8.8 -    Constructs terms corresponding to goals from
     8.9 -    lifting theorems to quotient types.
    8.10 +Constructs terms corresponding to goals from lifting theorems to
    8.11 +quotient types.
    8.12  *)
    8.13  
    8.14  signature QUOTIENT_TERM =
    8.15 @@ -779,8 +779,4 @@
    8.16    lift_aux t
    8.17  end
    8.18  
    8.19 -
    8.20  end; (* structure *)
    8.21 -
    8.22 -
    8.23 -
     9.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 14:29:30 2010 +0100
     9.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 14:31:24 2010 +0100
     9.3 @@ -1,8 +1,7 @@
     9.4 -(*  Title:      quotient_typ.thy
     9.5 +(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
     9.6      Author:     Cezary Kaliszyk and Christian Urban
     9.7  
     9.8 -    Definition of a quotient type.
     9.9 -
    9.10 +Definition of a quotient type.
    9.11  *)
    9.12  
    9.13  signature QUOTIENT_TYPE =