# HG changeset patch
# User wenzelm
# Date 1491592638 -7200
# Node ID 378175f4432812d494d31b146640a9c122f9f341
# Parent  e62b1af601f04fe83eb5680e453749cdcd7bd8ad
tuned headers;

diff -r e62b1af601f0 -r 378175f44328 src/HOL/Algebra/More_Ring.thy
--- a/src/HOL/Algebra/More_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Algebra/More_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Algebra/More_Group.thy
+(*  Title:      HOL/Algebra/More_Ring.thy
     Author:     Jeremy Avigad
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
+(*  Title:      HOL/Computational_Algebra/Euclidean_Algorithm.thy
     Author:     Manuel Eberl, TU Muenchen
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Number_Theory/Factorial_Ring.thy
+(*  Title:      HOL/Computational_Algebra/Factorial_Ring.thy
     Author:     Manuel Eberl, TU Muenchen
     Author:     Florian Haftmann, TU Muenchen
 *)
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Field_as_Ring.thy
--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Field_as_Ring.thy
+(*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
     Author:     Manuel Eberl
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Formal_Power_Series.thy
+(*  Title:      HOL/Computational_Algebra/Formal_Power_Series.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Fraction_Field.thy
--- a/src/HOL/Computational_Algebra/Fraction_Field.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Fraction_Field.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Fraction_Field.thy
+(*  Title:      HOL/Computational_Algebra/Fraction_Field.thy
     Author:     Amine Chaieb, University of Cambridge
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,6 @@
-(* Author: Amine Chaieb, TU Muenchen *)
+(*  Title:      HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
+    Author:     Amine Chaieb, TU Muenchen
+*)
 
 section \<open>Fundamental Theorem of Algebra\<close>
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Normalized_Fraction.thy
+(*  Title:      HOL/Computational_Algebra/Normalized_Fraction.thy
     Author:     Manuel Eberl
 *)
 
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Polynomial.thy
+(*  Title:      HOL/Computational_Algebra/Polynomial.thy
     Author:     Brian Huffman
     Author:     Clemens Ballarin
     Author:     Amine Chaieb
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Polynomial_FPS.thy
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,7 +1,5 @@
-(*  Title:      HOL/Library/Polynomial_FPS.thy
+(*  Title:      HOL/Computational_Algebra/Polynomial_FPS.thy
     Author:     Manuel Eberl, TU München
-  
-Converting polynomials to formal power series.
 *)
 
 section \<open>Converting polynomials to formal power series\<close>
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Polynomial_Factorial.thy
+(*  Title:      HOL/Computational_Algebra/Polynomial_Factorial.thy
     Author:     Brian Huffman
     Author:     Clemens Ballarin
     Author:     Amine Chaieb
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,9 +1,13 @@
-(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
-                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
-                Manuel Eberl
+(*  Title:      HOL/Computational_Algebra/Primes.thy
+    Author:     Christophe Tabacznyj
+    Author:     Lawrence C. Paulson
+    Author:     Amine Chaieb
+    Author:     Thomas M. Rasmussen
+    Author:     Jeremy Avigad
+    Author:     Tobias Nipkow
+    Author:     Manuel Eberl
 
-
-This file deals with properties of primes. Definitions and lemmas are
+This theory deals with properties of primes. Definitions and lemmas are
 proved uniformly for the natural numbers and integers.
 
 This file combines and revises a number of prior developments.
@@ -32,7 +36,6 @@
 Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
 *)
 
-
 section \<open>Primes\<close>
 
 theory Primes
diff -r e62b1af601f0 -r 378175f44328 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Apr 07 21:07:07 2017 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Apr 07 21:17:18 2017 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Number_Theory/Quadratic_Reciprocity.thy
+(*  Title:      HOL/Number_Theory/Gauss.thy
     Authors:    Jeremy Avigad, David Gray, and Adam Kramer
 
 Ported by lcp but unfinished.