# HG changeset patch
# User wenzelm
# Date 1269187951 -3600
# Node ID b5522b51cb1ecd19453a5e89f01242a18be9e41b
# Parent  5443079512eaf3be28c8d4213b64a9cb5c549ac6
standard headers;

diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,13 +1,11 @@
-(*
-  Title:     HOL/Algebra/AbelCoset.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/AbelCoset.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory AbelCoset
 imports Coset Ring
 begin
 
-
 subsection {* More Lifting from Groups to Abelian Groups *}
 
 subsubsection {* Definitions *}
@@ -520,6 +518,7 @@
 text {* The isomorphism theorems have been omitted from lifting, at
   least for now *}
 
+
 subsubsection{*The First Isomorphism Theorem*}
 
 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
@@ -642,6 +641,7 @@
 by (rule group_hom.FactGroup_iso[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
+
 subsubsection {* Cosets *}
 
 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
@@ -726,7 +726,6 @@
     folded A_RCOSETS_def, simplified monoid_record_simps])
 
 
-
 subsubsection {* Addition of Subgroups *}
 
 lemma (in abelian_monoid) set_add_closed:
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Bij.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -2,8 +2,9 @@
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-theory Bij imports Group begin
-
+theory Bij
+imports Group
+begin
 
 section {* Bijections of a Set, Permutation and Automorphism Groups *}
 
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,11 @@
-(*
-  Title:  Algebra/Congruence.thy
-  Author: Clemens Ballarin, started 3 January 2008
-  Copyright: Clemens Ballarin
+(*  Title:      Algebra/Congruence.thy
+    Author:     Clemens Ballarin, started 3 January 2008
+    Copyright:  Clemens Ballarin
 *)
 
-theory Congruence imports Main begin
+theory Congruence
+imports Main
+begin
 
 section {* Objects *}
 
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,12 @@
 (*  Title:      HOL/Algebra/Coset.thy
-    Author:     Florian Kammueller, with new proofs by L C Paulson, and
-                Stephan Hohe
+    Author:     Florian Kammueller
+    Author:     L C Paulson
+    Author:     Stephan Hohe
 *)
 
-theory Coset imports Group begin
-
+theory Coset
+imports Group
+begin
 
 section {*Cosets and Quotient Groups*}
 
@@ -653,6 +655,7 @@
   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
 qed
 
+
 subsubsection{*Two Distinct Right Cosets are Disjoint*}
 
 lemma (in group) rcos_equation:
@@ -678,6 +681,7 @@
     done
 qed
 
+
 subsection {* Further lemmas for @{text "r_congruent"} *}
 
 text {* The relation is a congruence *}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     Divisibility in monoids and rings
-  Author:    Clemens Ballarin, started 18 July 2008
+(*  Title:      Divisibility in monoids and rings
+    Author:     Clemens Ballarin, started 18 July 2008
 
 Based on work by Stephan Hohe.
 *)
@@ -156,6 +155,7 @@
       show "a \<in> Units G" by (simp add: Units_def, fast)
 qed
 
+
 subsection {* Divisibility and Association *}
 
 subsubsection {* Function definitions *}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,8 @@
 (*  Title:      HOL/Algebra/Exponent.thy
-    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Author:     Florian Kammueller
+    Author:     L C Paulson
 
-    exponent p s   yields the greatest power of p that divides s.
+exponent p s   yields the greatest power of p that divides s.
 *)
 
 theory Exponent
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -4,8 +4,9 @@
 This file is largely based on HOL/Finite_Set.thy.
 *)
 
-theory FiniteProduct imports Group begin
-
+theory FiniteProduct
+imports Group
+begin
 
 subsection {* Product Operator for Commutative Monoids *}
 
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:  HOL/Algebra/Group.thy
-  Author: Clemens Ballarin, started 4 February 2003
+(*  Title:      HOL/Algebra/Group.thy
+    Author:     Clemens Ballarin, started 4 February 2003
 
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
@@ -9,7 +8,6 @@
 imports Lattice FuncSet
 begin
 
-
 section {* Monoids and Groups *}
 
 subsection {* Definitions *}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/CIdeal.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/CIdeal.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory Ideal
@@ -45,6 +44,7 @@
   done
 qed
 
+
 subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
 
 definition
@@ -71,6 +71,7 @@
   show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
 qed
 
+
 subsubsection {* Maximal Ideals *}
 
 locale maximalideal = ideal +
@@ -93,6 +94,7 @@
     (rule is_ideal, rule I_notcarr, rule I_maximal)
 qed
 
+
 subsubsection {* Prime Ideals *}
 
 locale primeideal = ideal + cring +
@@ -139,6 +141,7 @@
     done
 qed
 
+
 subsection {* Special Ideals *}
 
 lemma (in ring) zeroideal:
@@ -867,6 +870,7 @@
   qed
 qed
 
+
 subsection {* Derived Theorems *}
 
 --"A non-zero cring that has only the two trivial ideals is a field"
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,13 +1,11 @@
-(*
-  Title:     HOL/Algebra/IntRing.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/IntRing.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory IntRing
 imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
 begin
 
-
 section {* The Ring of Integers *}
 
 subsection {* Some properties of @{typ int} *}
@@ -49,6 +47,8 @@
  apply (unfold int_ring_def, simp+)
 done
 *)
+
+
 subsection {* Interpretations *}
 
 text {* Since definitions of derived operations are global, their
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,12 +1,13 @@
-(*
-  Title:     HOL/Algebra/Lattice.thy
-  Author:    Clemens Ballarin, started 7 November 2003
-  Copyright: Clemens Ballarin
+(*  Title:      HOL/Algebra/Lattice.thy
+    Author:     Clemens Ballarin, started 7 November 2003
+    Copyright:  Clemens Ballarin
 
 Most congruence rules by Stephan Hohe.
 *)
 
-theory Lattice imports Congruence begin
+theory Lattice
+imports Congruence
+begin
 
 section {* Orders and Lattices *}
 
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Module.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -3,8 +3,9 @@
     Copyright:  Clemens Ballarin
 *)
 
-theory Module imports Ring begin
-
+theory Module
+imports Ring
+begin
 
 section {* Modules over an Abelian Group *}
 
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/QuotRing.thy
-  Author:    Stephan Hohe
+(*  Title:      HOL/Algebra/QuotRing.thy
+    Author:     Stephan Hohe
 *)
 
 theory QuotRing
@@ -180,6 +179,7 @@
 done
 qed
 
+
 subsection {* Factorization over Prime Ideals *}
 
 text {* The quotient ring generated by a prime ideal is a domain *}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/README.html	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    The Isabelle Algebraic Library
-    $Id$
-    Author: Clemens Ballarin, started 24 September 1999
+(*  Author: Clemens Ballarin, started 24 September 1999
+
+The Isabelle Algebraic Library.
 *)
 
 (* Preliminaries from set and number theory *)
@@ -23,8 +22,7 @@
 ];
 
 
-(*** Old development, based on axiomatic type classes.
-     Will be withdrawn in future. ***)
+(*** Old development, based on axiomatic type classes ***)
 
 no_document use_thys [
   "abstract/Abstract",  (*The ring theory*)
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-  Title:     The algebraic hierarchy of rings
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      The algebraic hierarchy of rings
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 *)
 
 theory Ring
@@ -9,7 +8,6 @@
 uses ("ringsimp.ML")
 begin
 
-
 section {* The Algebraic Hierarchy of Rings *}
 
 subsection {* Abelian Groups *}
@@ -601,6 +599,7 @@
   from R show ?thesis by algebra
 qed
 
+
 subsubsection {* Sums over Finite Sets *}
 
 lemma (in ring) finsum_ldistr:
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/RingHom.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/RingHom.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory RingHom
@@ -100,6 +99,7 @@
     (rule R.is_cring, rule S.is_cring, rule homh)
 qed
 
+
 subsection {* The Kernel of a Ring Homomorphism *}
 
 --"the kernel of a ring homomorphism is an ideal"
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,10 @@
 (*  Title:      HOL/Algebra/Sylow.thy
-    ID:         $Id$
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-theory Sylow imports Coset Exponent begin
+theory Sylow
+imports Coset Exponent
+begin
 
 text {*
   See also \cite{Kammueller-Paulson:1999}.
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-  Title:     HOL/Algebra/UnivPoly.thy
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      HOL/Algebra/UnivPoly.thy
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 
 Contributions, in particular on long division, by Jesus Aransay.
 *)
@@ -10,7 +9,6 @@
 imports Module RingHom
 begin
 
-
 section {* Univariate Polynomials *}
 
 text {*
@@ -429,7 +427,8 @@
     using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
 qed (simp_all add: R1 R2)
 
-subsection{*Polynomials over a commutative ring for a commutative ring*}
+
+subsection {*Polynomials over a commutative ring for a commutative ring*}
 
 theorem UP_cring:
   "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
@@ -1474,6 +1473,7 @@
 lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>" 
   using lcoeff_nonzero [OF p_not_zero p_in_R] .
 
+
 subsection{*The long division algorithm: some previous facts.*}
 
 lemma coeff_minus [simp]:
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/Abstract.thy
--- a/src/HOL/Algebra/abstract/Abstract.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Abstract.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Summary theory of the development of abstract algebra
-    $Id$
-    Author: Clemens Ballarin, started 17 July 1997
+(*  Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of abstract algebra.
 *)
 
 theory Abstract
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/Factor.thy
--- a/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Factorisation within a factorial domain
-    $Id$
-    Author: Clemens Ballarin, started 25 November 1997
+(*  Author: Clemens Ballarin, started 25 November 1997
+
+Factorisation within a factorial domain.
 *)
 
-theory Factor imports Ring2 begin
+theory Factor
+imports Ring2
+begin
 
 definition
   Factorisation :: "['a::ring, 'a list, 'a] => bool" where
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/Field.thy
--- a/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Properties of abstract class field
-    Author: Clemens Ballarin, started 15 November 1997
+(*  Author: Clemens Ballarin, started 15 November 1997
+
+Properties of abstract class field.
 *)
 
-theory Field imports Factor PID begin
+theory Field
+imports Factor PID
+begin
 
 instance field < "domain"
   apply intro_classes
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Ideals for commutative rings
-    Author: Clemens Ballarin, started 24 September 1999
+(*  Author: Clemens Ballarin, started 24 September 1999
+
+Ideals for commutative rings.
 *)
 
-theory Ideal2 imports Ring2 begin
+theory Ideal2
+imports Ring2
+begin
 
 definition
   is_ideal :: "('a::ring) set => bool" where
@@ -28,8 +30,8 @@
 (* is_ideal *)
 
 lemma is_idealI:
-  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;  
-      !! a. a:I ==> - a : I; 0 : I;  
+  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
+      !! a. a:I ==> - a : I; 0 : I;
       !! a r. a:I ==> a * r : I |] ==> is_ideal I"
   unfolding is_ideal_def by blast
 
@@ -241,7 +243,7 @@
   apply force
   done
 
-lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]  
+lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
     ==> is_ideal (Union (I`UNIV))"
   apply (rule is_idealI)
      apply auto
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/PID.thy
--- a/src/HOL/Algebra/abstract/PID.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/PID.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Principle ideal domains
-    Author: Clemens Ballarin, started 5 October 1999
+(*  Author: Clemens Ballarin, started 5 October 1999
+
+Principle ideal domains.
 *)
 
-theory PID imports Ideal2 begin
+theory PID
+imports Ideal2
+begin
 
 instance pid < factorial
   apply intro_classes
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/abstract/RingHomo.thy
--- a/src/HOL/Algebra/abstract/RingHomo.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Ring homomorphism
-    $Id$
-    Author: Clemens Ballarin, started 15 April 1997
+(*  Author: Clemens Ballarin, started 15 April 1997
+
+Ring homomorphism.
 *)
 
 header {* Ring homomorphism *}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/document/root.tex
--- a/src/HOL/Algebra/document/root.tex	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/document/root.tex	Sun Mar 21 17:12:31 2010 +0100
@@ -1,5 +1,3 @@
-% $Id$
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Experimental theory: long division of polynomials
-    Author: Clemens Ballarin, started 23 June 1999
+(*  Author: Clemens Ballarin, started 23 June 1999
+
+Experimental theory: long division of polynomials.
 *)
 
-theory LongDiv imports PolyHomo begin
+theory LongDiv
+imports PolyHomo
+begin
 
 definition
   lcoeff :: "'a::ring up => 'a" where
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Universal property and evaluation homomorphism of univariate polynomials
-    $Id$
-    Author: Clemens Ballarin, started 15 April 1997
+(*  Author: Clemens Ballarin, started 15 April 1997
+
+Universal property and evaluation homomorphism of univariate polynomials.
 *)
 
-theory PolyHomo imports UnivPoly2 begin
+theory PolyHomo
+imports UnivPoly2
+begin
 
 definition
   EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/poly/Polynomial.thy
--- a/src/HOL/Algebra/poly/Polynomial.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/poly/Polynomial.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Summary theory of the development of (not instantiated) polynomials
-    $Id$
-    Author: Clemens Ballarin, started 17 July 1997
+(*  Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of (not instantiated) polynomials.
 *)
 
 theory Polynomial
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 17:12:31 2010 +0100
@@ -1,7 +1,6 @@
-(*
-  Title:     Univariate Polynomials
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      Univariate Polynomials
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 *)
 
 header {* Univariate Polynomials *}
@@ -15,6 +14,7 @@
 
 declare strong_setsum_cong [cong]
 
+
 section {* Definition of type up *}
 
 definition
@@ -479,6 +479,7 @@
   finally show ?thesis .
 qed
 
+
 section {* The degree function *}
 
 definition
diff -r 5443079512ea -r b5522b51cb1e src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Sun Mar 21 16:51:37 2010 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Sun Mar 21 17:12:31 2010 +0100
@@ -1,4 +1,4 @@
-(*  Author:    Clemens Ballarin
+(*  Author:     Clemens Ballarin
 
 Normalisation method for locales ring and cring.
 *)