tuned headers;
authorwenzelm
Fri Apr 07 21:17:18 2017 +0200 (2017-04-07)
changeset 65435378175f44328
parent 65434 e62b1af601f0
child 65436 1fd2dca8eb60
child 65437 b8fc7e2e1b35
child 65439 862bfd2b4fd4
tuned headers;
src/HOL/Algebra/More_Ring.thy
src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/Computational_Algebra/Field_as_Ring.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Computational_Algebra/Fraction_Field.thy
src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
src/HOL/Computational_Algebra/Normalized_Fraction.thy
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/Computational_Algebra/Polynomial_FPS.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Number_Theory/Gauss.thy
     1.1 --- a/src/HOL/Algebra/More_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
     1.2 +++ b/src/HOL/Algebra/More_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Algebra/More_Group.thy
     1.5 +(*  Title:      HOL/Algebra/More_Ring.thy
     1.6      Author:     Jeremy Avigad
     1.7  *)
     1.8  
     2.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Fri Apr 07 21:07:07 2017 +0200
     2.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Fri Apr 07 21:17:18 2017 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
     2.5 +(*  Title:      HOL/Computational_Algebra/Euclidean_Algorithm.thy
     2.6      Author:     Manuel Eberl, TU Muenchen
     2.7  *)
     2.8  
     3.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
     3.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     3.5 +(*  Title:      HOL/Computational_Algebra/Factorial_Ring.thy
     3.6      Author:     Manuel Eberl, TU Muenchen
     3.7      Author:     Florian Haftmann, TU Muenchen
     3.8  *)
     4.1 --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Fri Apr 07 21:07:07 2017 +0200
     4.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Fri Apr 07 21:17:18 2017 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Library/Field_as_Ring.thy
     4.5 +(*  Title:      HOL/Computational_Algebra/Field_as_Ring.thy
     4.6      Author:     Manuel Eberl
     4.7  *)
     4.8  
     5.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 07 21:07:07 2017 +0200
     5.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 07 21:17:18 2017 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title:      HOL/Library/Formal_Power_Series.thy
     5.5 +(*  Title:      HOL/Computational_Algebra/Formal_Power_Series.thy
     5.6      Author:     Amine Chaieb, University of Cambridge
     5.7  *)
     5.8  
     6.1 --- a/src/HOL/Computational_Algebra/Fraction_Field.thy	Fri Apr 07 21:07:07 2017 +0200
     6.2 +++ b/src/HOL/Computational_Algebra/Fraction_Field.thy	Fri Apr 07 21:17:18 2017 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/Library/Fraction_Field.thy
     6.5 +(*  Title:      HOL/Computational_Algebra/Fraction_Field.thy
     6.6      Author:     Amine Chaieb, University of Cambridge
     6.7  *)
     6.8  
     7.1 --- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Fri Apr 07 21:07:07 2017 +0200
     7.2 +++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Fri Apr 07 21:17:18 2017 +0200
     7.3 @@ -1,4 +1,6 @@
     7.4 -(* Author: Amine Chaieb, TU Muenchen *)
     7.5 +(*  Title:      HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
     7.6 +    Author:     Amine Chaieb, TU Muenchen
     7.7 +*)
     7.8  
     7.9  section \<open>Fundamental Theorem of Algebra\<close>
    7.10  
     8.1 --- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Apr 07 21:07:07 2017 +0200
     8.2 +++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Fri Apr 07 21:17:18 2017 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/Library/Normalized_Fraction.thy
     8.5 +(*  Title:      HOL/Computational_Algebra/Normalized_Fraction.thy
     8.6      Author:     Manuel Eberl
     8.7  *)
     8.8  
     9.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Apr 07 21:07:07 2017 +0200
     9.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Apr 07 21:17:18 2017 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Library/Polynomial.thy
     9.5 +(*  Title:      HOL/Computational_Algebra/Polynomial.thy
     9.6      Author:     Brian Huffman
     9.7      Author:     Clemens Ballarin
     9.8      Author:     Amine Chaieb
    10.1 --- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 07 21:07:07 2017 +0200
    10.2 +++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 07 21:17:18 2017 +0200
    10.3 @@ -1,7 +1,5 @@
    10.4 -(*  Title:      HOL/Library/Polynomial_FPS.thy
    10.5 +(*  Title:      HOL/Computational_Algebra/Polynomial_FPS.thy
    10.6      Author:     Manuel Eberl, TU M√ľnchen
    10.7 -  
    10.8 -Converting polynomials to formal power series.
    10.9  *)
   10.10  
   10.11  section \<open>Converting polynomials to formal power series\<close>
    11.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Apr 07 21:07:07 2017 +0200
    11.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Fri Apr 07 21:17:18 2017 +0200
    11.3 @@ -1,4 +1,4 @@
    11.4 -(*  Title:      HOL/Library/Polynomial_Factorial.thy
    11.5 +(*  Title:      HOL/Computational_Algebra/Polynomial_Factorial.thy
    11.6      Author:     Brian Huffman
    11.7      Author:     Clemens Ballarin
    11.8      Author:     Amine Chaieb
    12.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Fri Apr 07 21:07:07 2017 +0200
    12.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Fri Apr 07 21:17:18 2017 +0200
    12.3 @@ -1,9 +1,13 @@
    12.4 -(*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
    12.5 -                Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow, 
    12.6 -                Manuel Eberl
    12.7 +(*  Title:      HOL/Computational_Algebra/Primes.thy
    12.8 +    Author:     Christophe Tabacznyj
    12.9 +    Author:     Lawrence C. Paulson
   12.10 +    Author:     Amine Chaieb
   12.11 +    Author:     Thomas M. Rasmussen
   12.12 +    Author:     Jeremy Avigad
   12.13 +    Author:     Tobias Nipkow
   12.14 +    Author:     Manuel Eberl
   12.15  
   12.16 -
   12.17 -This file deals with properties of primes. Definitions and lemmas are
   12.18 +This theory deals with properties of primes. Definitions and lemmas are
   12.19  proved uniformly for the natural numbers and integers.
   12.20  
   12.21  This file combines and revises a number of prior developments.
   12.22 @@ -32,7 +36,6 @@
   12.23  Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
   12.24  *)
   12.25  
   12.26 -
   12.27  section \<open>Primes\<close>
   12.28  
   12.29  theory Primes
    13.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Apr 07 21:07:07 2017 +0200
    13.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Fri Apr 07 21:17:18 2017 +0200
    13.3 @@ -1,4 +1,4 @@
    13.4 -(*  Title:      HOL/Number_Theory/Quadratic_Reciprocity.thy
    13.5 +(*  Title:      HOL/Number_Theory/Gauss.thy
    13.6      Authors:    Jeremy Avigad, David Gray, and Adam Kramer
    13.7  
    13.8  Ported by lcp but unfinished.