# HG changeset patch
# User ballarin
# Date 1052338053 -7200
# Node ID c8e9a89883ce2188165201f274b857106a5759f6
# Parent  9a4cb68e331503415b1437a7aa940419a0239e62
Small changes for release Isabelle 2003.

diff -r 9a4cb68e3315 -r c8e9a89883ce src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed May 07 17:46:04 2003 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed May 07 22:07:33 2003 +0200
@@ -10,11 +10,6 @@
 
 theory Group = FuncSet:
 
-(* axclass number < type
-
-instance nat :: number ..
-instance int :: number .. *)
-
 section {* From Magmas to Groups *}
 
 text {*
diff -r 9a4cb68e3315 -r c8e9a89883ce src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Wed May 07 17:46:04 2003 +0200
+++ b/src/HOL/Algebra/Module.thy	Wed May 07 22:07:33 2003 +0200
@@ -139,25 +139,4 @@
   finally show ?thesis .
 qed
 
-subsection {* Every Abelian Group is a Z-module *}
-
-(* Not all versions of pdflatex permit $\mathbb{Z}$ in bookmarks. *)
-
-text {* Not finished. *}
-
-constdefs
-  INTEG :: "int ring"
-  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
-
-(*
-  INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
-  "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
-    zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
-*)
-
-lemma cring_INTEG:
-  "cring INTEG"
-  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
-    zadd_zminus_inverse2 zadd_zmult_distrib)
-
 end
diff -r 9a4cb68e3315 -r c8e9a89883ce src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html	Wed May 07 17:46:04 2003 +0200
+++ b/src/HOL/Algebra/README.html	Wed May 07 22:07:33 2003 +0200
@@ -3,7 +3,12 @@
 
 <H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
 
-This directory presents proofs in classical algebra.  
+This directory contains proofs in classical algebra.  It is intended
+as a base for any algebraic development in Isabelle.  Emphasis is on
+reusability.  This is achieved by modelling algebraic structures
+as first-class citizens of the logic (not axiomatic type classes, say).
+The library is expected to grow in future releases of Isabelle.
+Contributions are welcome.
 
 <H2>GroupTheory, including Sylow's Theorem</H2>
 
diff -r 9a4cb68e3315 -r c8e9a89883ce src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed May 07 17:46:04 2003 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed May 07 22:07:33 2003 +0200
@@ -1515,6 +1515,15 @@
   by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
     cring.axioms prems)
 
+constdefs
+  INTEG :: "int ring"
+  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+
+lemma cring_INTEG:
+  "cring INTEG"
+  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
+    zadd_zminus_inverse2 zadd_zmult_distrib)
+
 lemma INTEG_id:
   "ring_hom_UP_cring INTEG INTEG id"
   by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)