--- a/src/HOL/Algebra/IntRing.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy Mon Mar 01 13:40:23 2010 +0100
@@ -22,8 +22,7 @@
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
-constdefs
- int_ring :: "int ring" ("\<Z>")
+definition int_ring :: "int ring" ("\<Z>") where
"int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
lemma int_Zcarr [intro!, simp]:
@@ -324,8 +323,7 @@
subsection {* Ideals and the Modulus *}
-constdefs
- ZMod :: "int => int => int set"
+definition ZMod :: "int => int => int set" where
"ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
lemmas ZMod_defs =
@@ -407,8 +405,7 @@
subsection {* Factorization *}
-constdefs
- ZFact :: "int \<Rightarrow> int set ring"
+definition ZFact :: "int \<Rightarrow> int set ring" where
"ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
lemmas ZFact_defs = ZFact_def FactRing_def