# HG changeset patch
# User wenzelm
# Date 1530608437 -7200
# Node ID b9b9e29858782ba21c31d49417b9a7fc86da064a
# Parent  0793e5ad25eca35bd04d2332b8460e3ca5c004a9
more standard headers;
tuned whitespace;

diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Algebra.thy
--- a/src/HOL/Algebra/Algebra.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Algebra.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Algebra/Algebra *)
+(*  Title:      HOL/Algebra/Algebra.thy *)
 
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Chinese_Remainder.thy
--- a/src/HOL/Algebra/Chinese_Remainder.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Chinese_Remainder.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Chinese_Remainder.thy                                          *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Chinese_Remainder.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Chinese_Remainder
   imports QuotRing Ideal_Product
-    
 begin
 
 section \<open>Chinese Remainder Theorem\<close>
@@ -1204,4 +1202,4 @@
           is_ring by (simp add: ring_hom_ringI2) 
 qed
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Coset.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Algebra/Coset.thy
-    Authors:     Florian Kammueller, L C Paulson, Stephan Hohe
+    Authors:    Florian Kammueller, L C Paulson, Stephan Hohe
+
 With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
 *)
 
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Cycles.thy
--- a/src/HOL/Algebra/Cycles.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Cycles.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Cycles.thy                                                     *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Cycles.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Cycles
   imports "HOL-Library.Permutations" "HOL-Library.FuncSet"
-    
 begin
 
 section \<open>Cycles\<close>
@@ -753,4 +751,4 @@
   shows "cycle_decomp S p"
   using assms cycle_decomposition_aux by blast
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Embedded_Algebras.thy
--- a/src/HOL/Algebra/Embedded_Algebras.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Embedded_Algebras.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Embedded_Algebras.thy                                          *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Embedded_Algebras.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Embedded_Algebras
   imports Subrings Generated_Groups
-
 begin
 
 section \<open>Definitions\<close>
@@ -1315,4 +1313,4 @@
 qed
 *)
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Exact_Sequence.thy
--- a/src/HOL/Algebra/Exact_Sequence.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Exact_Sequence.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Exact_Sequence.thy                                             *)
-(* Author:     Martin Baillon                                                 *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Exact_Sequence.thy
+    Author:     Martin Baillon
+*)
 
 theory Exact_Sequence
   imports Group Coset Solvable_Groups
-    
 begin
 
 section \<open>Exact Sequences\<close>
@@ -176,4 +174,3 @@
   using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast
 
 end
-         
\ No newline at end of file
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Generated_Fields.thy
--- a/src/HOL/Algebra/Generated_Fields.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Generated_Fields.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,12 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Generated_Fields.thy                                           *)
-(* Author:     Martin Baillon                                                 *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Generated_Fields.thy
+    Author:     Martin Baillon
+*)
 
 theory Generated_Fields
-
 imports Generated_Rings Subrings Multiplicative_Group
-
 begin
 
 inductive_set
@@ -184,7 +181,4 @@
         subfield_gen_incl[OF carrier_is_subfield assms(1) _ assms(2)] subfieldE(1)[OF assms(1)]
   by force
 
-
-
 end
-
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Generated_Groups.thy
--- a/src/HOL/Algebra/Generated_Groups.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Generated_Groups.thy                                           *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Generated_Groups.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Generated_Groups
   imports Group Coset
-
 begin
 
 section\<open>Generated Groups\<close>
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Group_Action.thy
--- a/src/HOL/Algebra/Group_Action.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Group_Action.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,9 +1,9 @@
-(* Title:      Group_Action.thy                                               *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
+(*  Title:      HOL/Algebra/Group_Action.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Group_Action
 imports Bij Coset Congruence
-
 begin
 
 section \<open>Group Actions\<close>
@@ -922,4 +922,4 @@
   using induced_homomorphism assms group.subgroup_imp_group group_BijGroup
         group_hom group_hom.axioms(1) group_hom_axioms_def by blast
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Ideal_Product.thy
--- a/src/HOL/Algebra/Ideal_Product.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Ideal_Product.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Ideal_Product.thy                                              *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Ideal_Product.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Ideal_Product
   imports Ideal
-    
 begin
 
 section \<open>Product of Ideals\<close>
@@ -587,4 +585,4 @@
     using assms is_cring by (simp add: primeidealI)
 qed
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Polynomials.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Polynomials.thy                                                *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Polynomials.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Polynomials
   imports Ring Ring_Divisibility Subrings
-
 begin
 
 section \<open>Polynomials\<close>
@@ -1851,5 +1849,4 @@
          simp add: univ_poly_def degree_def
          simp del: poly_add.simps poly_mult.simps)
 
-
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Algebra/QuotRing.thy
     Author:     Stephan Hohe
     Author:     Paulo Emílio de Vilhena
-
 *)
 
 theory QuotRing
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Ring.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Algebra/Ring.thy
     Author:     Clemens Ballarin, started 9 December 1996
 
-With contributions by Martin Baillon
+With contributions by Martin Baillon.
 *)
 
 theory Ring
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Ring_Divisibility.thy
--- a/src/HOL/Algebra/Ring_Divisibility.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Ring_Divisibility.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Ring_Divisibility.thy                                          *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Ring_Divisibility.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Ring_Divisibility
 imports Ideal Divisibility QuotRing
-
 begin
 
 section \<open>Definitions ported from @{text "Multiplicative_Group.thy"}\<close>
@@ -803,4 +801,4 @@
     by blast
 qed
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Solvable_Groups.thy
--- a/src/HOL/Algebra/Solvable_Groups.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Solvable_Groups.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Solvable_Groups.thy                                            *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Solvable_Groups.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Solvable_Groups
   imports Group Coset Generated_Groups
-    
 begin
 
 inductive solvable_seq :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> bool" for G where
@@ -428,4 +426,4 @@
     unfolding solvable_def group_hom_def by (simp add: group.subgroup_self)
 qed
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Subrings.thy
--- a/src/HOL/Algebra/Subrings.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Subrings.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Subrings.thy                                                   *)
-(* Authors:    Martin Baillon and Paulo Emílio de Vilhena                     *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Subrings.thy
+    Authors:    Martin Baillon and Paulo Emílio de Vilhena
+*)
 
 theory Subrings
   imports Ring RingHom QuotRing Multiplicative_Group
-
 begin
 
 section \<open>Subrings\<close>
@@ -425,4 +423,4 @@
     using S.subfield_iff[of "h ` K"] K(1) ring_hom_memE(1)[OF homh] by blast
 qed
 
-end
\ No newline at end of file
+end
diff -r 0793e5ad25ec -r b9b9e2985878 src/HOL/Algebra/Sym_Groups.thy
--- a/src/HOL/Algebra/Sym_Groups.thy	Tue Jul 03 10:49:44 2018 +0200
+++ b/src/HOL/Algebra/Sym_Groups.thy	Tue Jul 03 11:00:37 2018 +0200
@@ -1,11 +1,9 @@
-(* ************************************************************************** *)
-(* Title:      Sym_Groups.th                                                  *)
-(* Author:     Paulo Emílio de Vilhena                                        *)
-(* ************************************************************************** *)
+(*  Title:      HOL/Algebra/Sym_Groups.thy
+    Author:     Paulo Emílio de Vilhena
+*)
 
 theory Sym_Groups
   imports Cycles Group Coset Generated_Groups Solvable_Groups
-    
 begin
 
 abbreviation inv' :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
@@ -661,4 +659,4 @@
           alt_group_not_solvable[OF assms] inj_on_id by blast
 qed
 
-end
\ No newline at end of file
+end