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