standard headers;
authorwenzelm
Sun Mar 21 17:12:31 2010 +0100 (2010-03-21)
changeset 35849b5522b51cb1e
parent 35848 5443079512ea
child 35850 dd2636f0f608
standard headers;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Bij.thy
src/HOL/Algebra/Congruence.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/QuotRing.thy
src/HOL/Algebra/README.html
src/HOL/Algebra/ROOT.ML
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/abstract/Abstract.thy
src/HOL/Algebra/abstract/Factor.thy
src/HOL/Algebra/abstract/Field.thy
src/HOL/Algebra/abstract/Ideal2.thy
src/HOL/Algebra/abstract/PID.thy
src/HOL/Algebra/abstract/RingHomo.thy
src/HOL/Algebra/document/root.tex
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/Algebra/poly/Polynomial.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Algebra/ringsimp.ML
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 16:51:37 2010 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 17:12:31 2010 +0100
     1.3 @@ -1,13 +1,11 @@
     1.4 -(*
     1.5 -  Title:     HOL/Algebra/AbelCoset.thy
     1.6 -  Author:    Stephan Hohe, TU Muenchen
     1.7 +(*  Title:      HOL/Algebra/AbelCoset.thy
     1.8 +    Author:     Stephan Hohe, TU Muenchen
     1.9  *)
    1.10  
    1.11  theory AbelCoset
    1.12  imports Coset Ring
    1.13  begin
    1.14  
    1.15 -
    1.16  subsection {* More Lifting from Groups to Abelian Groups *}
    1.17  
    1.18  subsubsection {* Definitions *}
    1.19 @@ -520,6 +518,7 @@
    1.20  text {* The isomorphism theorems have been omitted from lifting, at
    1.21    least for now *}
    1.22  
    1.23 +
    1.24  subsubsection{*The First Isomorphism Theorem*}
    1.25  
    1.26  text{*The quotient by the kernel of a homomorphism is isomorphic to the 
    1.27 @@ -642,6 +641,7 @@
    1.28  by (rule group_hom.FactGroup_iso[OF a_group_hom,
    1.29      folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
    1.30  
    1.31 +
    1.32  subsubsection {* Cosets *}
    1.33  
    1.34  text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
    1.35 @@ -726,7 +726,6 @@
    1.36      folded A_RCOSETS_def, simplified monoid_record_simps])
    1.37  
    1.38  
    1.39 -
    1.40  subsubsection {* Addition of Subgroups *}
    1.41  
    1.42  lemma (in abelian_monoid) set_add_closed:
     2.1 --- a/src/HOL/Algebra/Bij.thy	Sun Mar 21 16:51:37 2010 +0100
     2.2 +++ b/src/HOL/Algebra/Bij.thy	Sun Mar 21 17:12:31 2010 +0100
     2.3 @@ -2,8 +2,9 @@
     2.4      Author:     Florian Kammueller, with new proofs by L C Paulson
     2.5  *)
     2.6  
     2.7 -theory Bij imports Group begin
     2.8 -
     2.9 +theory Bij
    2.10 +imports Group
    2.11 +begin
    2.12  
    2.13  section {* Bijections of a Set, Permutation and Automorphism Groups *}
    2.14  
     3.1 --- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 16:51:37 2010 +0100
     3.2 +++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 21 17:12:31 2010 +0100
     3.3 @@ -1,10 +1,11 @@
     3.4 -(*
     3.5 -  Title:  Algebra/Congruence.thy
     3.6 -  Author: Clemens Ballarin, started 3 January 2008
     3.7 -  Copyright: Clemens Ballarin
     3.8 +(*  Title:      Algebra/Congruence.thy
     3.9 +    Author:     Clemens Ballarin, started 3 January 2008
    3.10 +    Copyright:  Clemens Ballarin
    3.11  *)
    3.12  
    3.13 -theory Congruence imports Main begin
    3.14 +theory Congruence
    3.15 +imports Main
    3.16 +begin
    3.17  
    3.18  section {* Objects *}
    3.19  
     4.1 --- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 16:51:37 2010 +0100
     4.2 +++ b/src/HOL/Algebra/Coset.thy	Sun Mar 21 17:12:31 2010 +0100
     4.3 @@ -1,10 +1,12 @@
     4.4  (*  Title:      HOL/Algebra/Coset.thy
     4.5 -    Author:     Florian Kammueller, with new proofs by L C Paulson, and
     4.6 -                Stephan Hohe
     4.7 +    Author:     Florian Kammueller
     4.8 +    Author:     L C Paulson
     4.9 +    Author:     Stephan Hohe
    4.10  *)
    4.11  
    4.12 -theory Coset imports Group begin
    4.13 -
    4.14 +theory Coset
    4.15 +imports Group
    4.16 +begin
    4.17  
    4.18  section {*Cosets and Quotient Groups*}
    4.19  
    4.20 @@ -653,6 +655,7 @@
    4.21    show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
    4.22  qed
    4.23  
    4.24 +
    4.25  subsubsection{*Two Distinct Right Cosets are Disjoint*}
    4.26  
    4.27  lemma (in group) rcos_equation:
    4.28 @@ -678,6 +681,7 @@
    4.29      done
    4.30  qed
    4.31  
    4.32 +
    4.33  subsection {* Further lemmas for @{text "r_congruent"} *}
    4.34  
    4.35  text {* The relation is a congruence *}
     5.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 16:51:37 2010 +0100
     5.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 17:12:31 2010 +0100
     5.3 @@ -1,6 +1,5 @@
     5.4 -(*
     5.5 -  Title:     Divisibility in monoids and rings
     5.6 -  Author:    Clemens Ballarin, started 18 July 2008
     5.7 +(*  Title:      Divisibility in monoids and rings
     5.8 +    Author:     Clemens Ballarin, started 18 July 2008
     5.9  
    5.10  Based on work by Stephan Hohe.
    5.11  *)
    5.12 @@ -156,6 +155,7 @@
    5.13        show "a \<in> Units G" by (simp add: Units_def, fast)
    5.14  qed
    5.15  
    5.16 +
    5.17  subsection {* Divisibility and Association *}
    5.18  
    5.19  subsubsection {* Function definitions *}
     6.1 --- a/src/HOL/Algebra/Exponent.thy	Sun Mar 21 16:51:37 2010 +0100
     6.2 +++ b/src/HOL/Algebra/Exponent.thy	Sun Mar 21 17:12:31 2010 +0100
     6.3 @@ -1,7 +1,8 @@
     6.4  (*  Title:      HOL/Algebra/Exponent.thy
     6.5 -    Author:     Florian Kammueller, with new proofs by L C Paulson
     6.6 +    Author:     Florian Kammueller
     6.7 +    Author:     L C Paulson
     6.8  
     6.9 -    exponent p s   yields the greatest power of p that divides s.
    6.10 +exponent p s   yields the greatest power of p that divides s.
    6.11  *)
    6.12  
    6.13  theory Exponent
     7.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 16:51:37 2010 +0100
     7.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 17:12:31 2010 +0100
     7.3 @@ -4,8 +4,9 @@
     7.4  This file is largely based on HOL/Finite_Set.thy.
     7.5  *)
     7.6  
     7.7 -theory FiniteProduct imports Group begin
     7.8 -
     7.9 +theory FiniteProduct
    7.10 +imports Group
    7.11 +begin
    7.12  
    7.13  subsection {* Product Operator for Commutative Monoids *}
    7.14  
     8.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 16:51:37 2010 +0100
     8.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 17:12:31 2010 +0100
     8.3 @@ -1,6 +1,5 @@
     8.4 -(*
     8.5 -  Title:  HOL/Algebra/Group.thy
     8.6 -  Author: Clemens Ballarin, started 4 February 2003
     8.7 +(*  Title:      HOL/Algebra/Group.thy
     8.8 +    Author:     Clemens Ballarin, started 4 February 2003
     8.9  
    8.10  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
    8.11  *)
    8.12 @@ -9,7 +8,6 @@
    8.13  imports Lattice FuncSet
    8.14  begin
    8.15  
    8.16 -
    8.17  section {* Monoids and Groups *}
    8.18  
    8.19  subsection {* Definitions *}
     9.1 --- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 16:51:37 2010 +0100
     9.2 +++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 21 17:12:31 2010 +0100
     9.3 @@ -1,6 +1,5 @@
     9.4 -(*
     9.5 -  Title:     HOL/Algebra/CIdeal.thy
     9.6 -  Author:    Stephan Hohe, TU Muenchen
     9.7 +(*  Title:      HOL/Algebra/CIdeal.thy
     9.8 +    Author:     Stephan Hohe, TU Muenchen
     9.9  *)
    9.10  
    9.11  theory Ideal
    9.12 @@ -45,6 +44,7 @@
    9.13    done
    9.14  qed
    9.15  
    9.16 +
    9.17  subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
    9.18  
    9.19  definition
    9.20 @@ -71,6 +71,7 @@
    9.21    show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
    9.22  qed
    9.23  
    9.24 +
    9.25  subsubsection {* Maximal Ideals *}
    9.26  
    9.27  locale maximalideal = ideal +
    9.28 @@ -93,6 +94,7 @@
    9.29      (rule is_ideal, rule I_notcarr, rule I_maximal)
    9.30  qed
    9.31  
    9.32 +
    9.33  subsubsection {* Prime Ideals *}
    9.34  
    9.35  locale primeideal = ideal + cring +
    9.36 @@ -139,6 +141,7 @@
    9.37      done
    9.38  qed
    9.39  
    9.40 +
    9.41  subsection {* Special Ideals *}
    9.42  
    9.43  lemma (in ring) zeroideal:
    9.44 @@ -867,6 +870,7 @@
    9.45    qed
    9.46  qed
    9.47  
    9.48 +
    9.49  subsection {* Derived Theorems *}
    9.50  
    9.51  --"A non-zero cring that has only the two trivial ideals is a field"
    10.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Mar 21 16:51:37 2010 +0100
    10.2 +++ b/src/HOL/Algebra/IntRing.thy	Sun Mar 21 17:12:31 2010 +0100
    10.3 @@ -1,13 +1,11 @@
    10.4 -(*
    10.5 -  Title:     HOL/Algebra/IntRing.thy
    10.6 -  Author:    Stephan Hohe, TU Muenchen
    10.7 +(*  Title:      HOL/Algebra/IntRing.thy
    10.8 +    Author:     Stephan Hohe, TU Muenchen
    10.9  *)
   10.10  
   10.11  theory IntRing
   10.12  imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
   10.13  begin
   10.14  
   10.15 -
   10.16  section {* The Ring of Integers *}
   10.17  
   10.18  subsection {* Some properties of @{typ int} *}
   10.19 @@ -49,6 +47,8 @@
   10.20   apply (unfold int_ring_def, simp+)
   10.21  done
   10.22  *)
   10.23 +
   10.24 +
   10.25  subsection {* Interpretations *}
   10.26  
   10.27  text {* Since definitions of derived operations are global, their
    11.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 16:51:37 2010 +0100
    11.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 17:12:31 2010 +0100
    11.3 @@ -1,12 +1,13 @@
    11.4 -(*
    11.5 -  Title:     HOL/Algebra/Lattice.thy
    11.6 -  Author:    Clemens Ballarin, started 7 November 2003
    11.7 -  Copyright: Clemens Ballarin
    11.8 +(*  Title:      HOL/Algebra/Lattice.thy
    11.9 +    Author:     Clemens Ballarin, started 7 November 2003
   11.10 +    Copyright:  Clemens Ballarin
   11.11  
   11.12  Most congruence rules by Stephan Hohe.
   11.13  *)
   11.14  
   11.15 -theory Lattice imports Congruence begin
   11.16 +theory Lattice
   11.17 +imports Congruence
   11.18 +begin
   11.19  
   11.20  section {* Orders and Lattices *}
   11.21  
    12.1 --- a/src/HOL/Algebra/Module.thy	Sun Mar 21 16:51:37 2010 +0100
    12.2 +++ b/src/HOL/Algebra/Module.thy	Sun Mar 21 17:12:31 2010 +0100
    12.3 @@ -3,8 +3,9 @@
    12.4      Copyright:  Clemens Ballarin
    12.5  *)
    12.6  
    12.7 -theory Module imports Ring begin
    12.8 -
    12.9 +theory Module
   12.10 +imports Ring
   12.11 +begin
   12.12  
   12.13  section {* Modules over an Abelian Group *}
   12.14  
    13.1 --- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 16:51:37 2010 +0100
    13.2 +++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 17:12:31 2010 +0100
    13.3 @@ -1,6 +1,5 @@
    13.4 -(*
    13.5 -  Title:     HOL/Algebra/QuotRing.thy
    13.6 -  Author:    Stephan Hohe
    13.7 +(*  Title:      HOL/Algebra/QuotRing.thy
    13.8 +    Author:     Stephan Hohe
    13.9  *)
   13.10  
   13.11  theory QuotRing
   13.12 @@ -180,6 +179,7 @@
   13.13  done
   13.14  qed
   13.15  
   13.16 +
   13.17  subsection {* Factorization over Prime Ideals *}
   13.18  
   13.19  text {* The quotient ring generated by a prime ideal is a domain *}
    14.1 --- a/src/HOL/Algebra/README.html	Sun Mar 21 16:51:37 2010 +0100
    14.2 +++ b/src/HOL/Algebra/README.html	Sun Mar 21 17:12:31 2010 +0100
    14.3 @@ -1,7 +1,5 @@
    14.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    14.5  
    14.6 -<!-- $Id$ -->
    14.7 -
    14.8  <HTML>
    14.9  
   14.10  <HEAD>
    15.1 --- a/src/HOL/Algebra/ROOT.ML	Sun Mar 21 16:51:37 2010 +0100
    15.2 +++ b/src/HOL/Algebra/ROOT.ML	Sun Mar 21 17:12:31 2010 +0100
    15.3 @@ -1,7 +1,6 @@
    15.4 -(*
    15.5 -    The Isabelle Algebraic Library
    15.6 -    $Id$
    15.7 -    Author: Clemens Ballarin, started 24 September 1999
    15.8 +(*  Author: Clemens Ballarin, started 24 September 1999
    15.9 +
   15.10 +The Isabelle Algebraic Library.
   15.11  *)
   15.12  
   15.13  (* Preliminaries from set and number theory *)
   15.14 @@ -23,8 +22,7 @@
   15.15  ];
   15.16  
   15.17  
   15.18 -(*** Old development, based on axiomatic type classes.
   15.19 -     Will be withdrawn in future. ***)
   15.20 +(*** Old development, based on axiomatic type classes ***)
   15.21  
   15.22  no_document use_thys [
   15.23    "abstract/Abstract",  (*The ring theory*)
    16.1 --- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 16:51:37 2010 +0100
    16.2 +++ b/src/HOL/Algebra/Ring.thy	Sun Mar 21 17:12:31 2010 +0100
    16.3 @@ -1,7 +1,6 @@
    16.4 -(*
    16.5 -  Title:     The algebraic hierarchy of rings
    16.6 -  Author:    Clemens Ballarin, started 9 December 1996
    16.7 -  Copyright: Clemens Ballarin
    16.8 +(*  Title:      The algebraic hierarchy of rings
    16.9 +    Author:     Clemens Ballarin, started 9 December 1996
   16.10 +    Copyright:  Clemens Ballarin
   16.11  *)
   16.12  
   16.13  theory Ring
   16.14 @@ -9,7 +8,6 @@
   16.15  uses ("ringsimp.ML")
   16.16  begin
   16.17  
   16.18 -
   16.19  section {* The Algebraic Hierarchy of Rings *}
   16.20  
   16.21  subsection {* Abelian Groups *}
   16.22 @@ -601,6 +599,7 @@
   16.23    from R show ?thesis by algebra
   16.24  qed
   16.25  
   16.26 +
   16.27  subsubsection {* Sums over Finite Sets *}
   16.28  
   16.29  lemma (in ring) finsum_ldistr:
    17.1 --- a/src/HOL/Algebra/RingHom.thy	Sun Mar 21 16:51:37 2010 +0100
    17.2 +++ b/src/HOL/Algebra/RingHom.thy	Sun Mar 21 17:12:31 2010 +0100
    17.3 @@ -1,6 +1,5 @@
    17.4 -(*
    17.5 -  Title:     HOL/Algebra/RingHom.thy
    17.6 -  Author:    Stephan Hohe, TU Muenchen
    17.7 +(*  Title:      HOL/Algebra/RingHom.thy
    17.8 +    Author:     Stephan Hohe, TU Muenchen
    17.9  *)
   17.10  
   17.11  theory RingHom
   17.12 @@ -100,6 +99,7 @@
   17.13      (rule R.is_cring, rule S.is_cring, rule homh)
   17.14  qed
   17.15  
   17.16 +
   17.17  subsection {* The Kernel of a Ring Homomorphism *}
   17.18  
   17.19  --"the kernel of a ring homomorphism is an ideal"
    18.1 --- a/src/HOL/Algebra/Sylow.thy	Sun Mar 21 16:51:37 2010 +0100
    18.2 +++ b/src/HOL/Algebra/Sylow.thy	Sun Mar 21 17:12:31 2010 +0100
    18.3 @@ -1,9 +1,10 @@
    18.4  (*  Title:      HOL/Algebra/Sylow.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Florian Kammueller, with new proofs by L C Paulson
    18.7  *)
    18.8  
    18.9 -theory Sylow imports Coset Exponent begin
   18.10 +theory Sylow
   18.11 +imports Coset Exponent
   18.12 +begin
   18.13  
   18.14  text {*
   18.15    See also \cite{Kammueller-Paulson:1999}.
    19.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 16:51:37 2010 +0100
    19.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 17:12:31 2010 +0100
    19.3 @@ -1,7 +1,6 @@
    19.4 -(*
    19.5 -  Title:     HOL/Algebra/UnivPoly.thy
    19.6 -  Author:    Clemens Ballarin, started 9 December 1996
    19.7 -  Copyright: Clemens Ballarin
    19.8 +(*  Title:      HOL/Algebra/UnivPoly.thy
    19.9 +    Author:     Clemens Ballarin, started 9 December 1996
   19.10 +    Copyright:  Clemens Ballarin
   19.11  
   19.12  Contributions, in particular on long division, by Jesus Aransay.
   19.13  *)
   19.14 @@ -10,7 +9,6 @@
   19.15  imports Module RingHom
   19.16  begin
   19.17  
   19.18 -
   19.19  section {* Univariate Polynomials *}
   19.20  
   19.21  text {*
   19.22 @@ -429,7 +427,8 @@
   19.23      using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
   19.24  qed (simp_all add: R1 R2)
   19.25  
   19.26 -subsection{*Polynomials over a commutative ring for a commutative ring*}
   19.27 +
   19.28 +subsection {*Polynomials over a commutative ring for a commutative ring*}
   19.29  
   19.30  theorem UP_cring:
   19.31    "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
   19.32 @@ -1474,6 +1473,7 @@
   19.33  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>" 
   19.34    using lcoeff_nonzero [OF p_not_zero p_in_R] .
   19.35  
   19.36 +
   19.37  subsection{*The long division algorithm: some previous facts.*}
   19.38  
   19.39  lemma coeff_minus [simp]:
    20.1 --- a/src/HOL/Algebra/abstract/Abstract.thy	Sun Mar 21 16:51:37 2010 +0100
    20.2 +++ b/src/HOL/Algebra/abstract/Abstract.thy	Sun Mar 21 17:12:31 2010 +0100
    20.3 @@ -1,7 +1,6 @@
    20.4 -(*
    20.5 -    Summary theory of the development of abstract algebra
    20.6 -    $Id$
    20.7 -    Author: Clemens Ballarin, started 17 July 1997
    20.8 +(*  Author: Clemens Ballarin, started 17 July 1997
    20.9 +
   20.10 +Summary theory of the development of abstract algebra.
   20.11  *)
   20.12  
   20.13  theory Abstract
    21.1 --- a/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 16:51:37 2010 +0100
    21.2 +++ b/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 17:12:31 2010 +0100
    21.3 @@ -1,10 +1,11 @@
    21.4 -(*
    21.5 -    Factorisation within a factorial domain
    21.6 -    $Id$
    21.7 -    Author: Clemens Ballarin, started 25 November 1997
    21.8 +(*  Author: Clemens Ballarin, started 25 November 1997
    21.9 +
   21.10 +Factorisation within a factorial domain.
   21.11  *)
   21.12  
   21.13 -theory Factor imports Ring2 begin
   21.14 +theory Factor
   21.15 +imports Ring2
   21.16 +begin
   21.17  
   21.18  definition
   21.19    Factorisation :: "['a::ring, 'a list, 'a] => bool" where
    22.1 --- a/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 16:51:37 2010 +0100
    22.2 +++ b/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 17:12:31 2010 +0100
    22.3 @@ -1,9 +1,11 @@
    22.4 -(*
    22.5 -    Properties of abstract class field
    22.6 -    Author: Clemens Ballarin, started 15 November 1997
    22.7 +(*  Author: Clemens Ballarin, started 15 November 1997
    22.8 +
    22.9 +Properties of abstract class field.
   22.10  *)
   22.11  
   22.12 -theory Field imports Factor PID begin
   22.13 +theory Field
   22.14 +imports Factor PID
   22.15 +begin
   22.16  
   22.17  instance field < "domain"
   22.18    apply intro_classes
    23.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Sun Mar 21 16:51:37 2010 +0100
    23.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy	Sun Mar 21 17:12:31 2010 +0100
    23.3 @@ -1,9 +1,11 @@
    23.4 -(*
    23.5 -    Ideals for commutative rings
    23.6 -    Author: Clemens Ballarin, started 24 September 1999
    23.7 +(*  Author: Clemens Ballarin, started 24 September 1999
    23.8 +
    23.9 +Ideals for commutative rings.
   23.10  *)
   23.11  
   23.12 -theory Ideal2 imports Ring2 begin
   23.13 +theory Ideal2
   23.14 +imports Ring2
   23.15 +begin
   23.16  
   23.17  definition
   23.18    is_ideal :: "('a::ring) set => bool" where
   23.19 @@ -28,8 +30,8 @@
   23.20  (* is_ideal *)
   23.21  
   23.22  lemma is_idealI:
   23.23 -  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;  
   23.24 -      !! a. a:I ==> - a : I; 0 : I;  
   23.25 +  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
   23.26 +      !! a. a:I ==> - a : I; 0 : I;
   23.27        !! a r. a:I ==> a * r : I |] ==> is_ideal I"
   23.28    unfolding is_ideal_def by blast
   23.29  
   23.30 @@ -241,7 +243,7 @@
   23.31    apply force
   23.32    done
   23.33  
   23.34 -lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]  
   23.35 +lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
   23.36      ==> is_ideal (Union (I`UNIV))"
   23.37    apply (rule is_idealI)
   23.38       apply auto
    24.1 --- a/src/HOL/Algebra/abstract/PID.thy	Sun Mar 21 16:51:37 2010 +0100
    24.2 +++ b/src/HOL/Algebra/abstract/PID.thy	Sun Mar 21 17:12:31 2010 +0100
    24.3 @@ -1,9 +1,11 @@
    24.4 -(*
    24.5 -    Principle ideal domains
    24.6 -    Author: Clemens Ballarin, started 5 October 1999
    24.7 +(*  Author: Clemens Ballarin, started 5 October 1999
    24.8 +
    24.9 +Principle ideal domains.
   24.10  *)
   24.11  
   24.12 -theory PID imports Ideal2 begin
   24.13 +theory PID
   24.14 +imports Ideal2
   24.15 +begin
   24.16  
   24.17  instance pid < factorial
   24.18    apply intro_classes
    25.1 --- a/src/HOL/Algebra/abstract/RingHomo.thy	Sun Mar 21 16:51:37 2010 +0100
    25.2 +++ b/src/HOL/Algebra/abstract/RingHomo.thy	Sun Mar 21 17:12:31 2010 +0100
    25.3 @@ -1,7 +1,6 @@
    25.4 -(*
    25.5 -    Ring homomorphism
    25.6 -    $Id$
    25.7 -    Author: Clemens Ballarin, started 15 April 1997
    25.8 +(*  Author: Clemens Ballarin, started 15 April 1997
    25.9 +
   25.10 +Ring homomorphism.
   25.11  *)
   25.12  
   25.13  header {* Ring homomorphism *}
    26.1 --- a/src/HOL/Algebra/document/root.tex	Sun Mar 21 16:51:37 2010 +0100
    26.2 +++ b/src/HOL/Algebra/document/root.tex	Sun Mar 21 17:12:31 2010 +0100
    26.3 @@ -1,5 +1,3 @@
    26.4 -% $Id$
    26.5 -
    26.6  \documentclass[11pt,a4paper]{article}
    26.7  \usepackage{graphicx}
    26.8  \usepackage{isabelle,isabellesym}
    27.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Sun Mar 21 16:51:37 2010 +0100
    27.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Sun Mar 21 17:12:31 2010 +0100
    27.3 @@ -1,9 +1,11 @@
    27.4 -(*
    27.5 -    Experimental theory: long division of polynomials
    27.6 -    Author: Clemens Ballarin, started 23 June 1999
    27.7 +(*  Author: Clemens Ballarin, started 23 June 1999
    27.8 +
    27.9 +Experimental theory: long division of polynomials.
   27.10  *)
   27.11  
   27.12 -theory LongDiv imports PolyHomo begin
   27.13 +theory LongDiv
   27.14 +imports PolyHomo
   27.15 +begin
   27.16  
   27.17  definition
   27.18    lcoeff :: "'a::ring up => 'a" where
    28.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Sun Mar 21 16:51:37 2010 +0100
    28.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Sun Mar 21 17:12:31 2010 +0100
    28.3 @@ -1,10 +1,11 @@
    28.4 -(*
    28.5 -    Universal property and evaluation homomorphism of univariate polynomials
    28.6 -    $Id$
    28.7 -    Author: Clemens Ballarin, started 15 April 1997
    28.8 +(*  Author: Clemens Ballarin, started 15 April 1997
    28.9 +
   28.10 +Universal property and evaluation homomorphism of univariate polynomials.
   28.11  *)
   28.12  
   28.13 -theory PolyHomo imports UnivPoly2 begin
   28.14 +theory PolyHomo
   28.15 +imports UnivPoly2
   28.16 +begin
   28.17  
   28.18  definition
   28.19    EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
    29.1 --- a/src/HOL/Algebra/poly/Polynomial.thy	Sun Mar 21 16:51:37 2010 +0100
    29.2 +++ b/src/HOL/Algebra/poly/Polynomial.thy	Sun Mar 21 17:12:31 2010 +0100
    29.3 @@ -1,7 +1,6 @@
    29.4 -(*
    29.5 -    Summary theory of the development of (not instantiated) polynomials
    29.6 -    $Id$
    29.7 -    Author: Clemens Ballarin, started 17 July 1997
    29.8 +(*  Author: Clemens Ballarin, started 17 July 1997
    29.9 +
   29.10 +Summary theory of the development of (not instantiated) polynomials.
   29.11  *)
   29.12  
   29.13  theory Polynomial
    30.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 16:51:37 2010 +0100
    30.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 17:12:31 2010 +0100
    30.3 @@ -1,7 +1,6 @@
    30.4 -(*
    30.5 -  Title:     Univariate Polynomials
    30.6 -  Author:    Clemens Ballarin, started 9 December 1996
    30.7 -  Copyright: Clemens Ballarin
    30.8 +(*  Title:      Univariate Polynomials
    30.9 +    Author:     Clemens Ballarin, started 9 December 1996
   30.10 +    Copyright:  Clemens Ballarin
   30.11  *)
   30.12  
   30.13  header {* Univariate Polynomials *}
   30.14 @@ -15,6 +14,7 @@
   30.15  
   30.16  declare strong_setsum_cong [cong]
   30.17  
   30.18 +
   30.19  section {* Definition of type up *}
   30.20  
   30.21  definition
   30.22 @@ -479,6 +479,7 @@
   30.23    finally show ?thesis .
   30.24  qed
   30.25  
   30.26 +
   30.27  section {* The degree function *}
   30.28  
   30.29  definition
    31.1 --- a/src/HOL/Algebra/ringsimp.ML	Sun Mar 21 16:51:37 2010 +0100
    31.2 +++ b/src/HOL/Algebra/ringsimp.ML	Sun Mar 21 17:12:31 2010 +0100
    31.3 @@ -1,4 +1,4 @@
    31.4 -(*  Author:    Clemens Ballarin
    31.5 +(*  Author:     Clemens Ballarin
    31.6  
    31.7  Normalisation method for locales ring and cring.
    31.8  *)