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