--- 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:
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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
--- 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 *}
--- 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 *}
--- 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"
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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>
--- 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*)
--- 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:
--- 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"
--- 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}.
--- 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]:
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *}
--- 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}
--- 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
--- 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
--- 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
--- 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
--- 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.
*)