--- a/src/HOL/Algebra/IntRing.thy Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy Sun Mar 21 16:51:37 2010 +0100
@@ -22,8 +22,9 @@
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
-definition int_ring :: "int ring" ("\<Z>") where
- "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+definition
+ int_ring :: "int ring" ("\<Z>") where
+ "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
lemma int_Zcarr [intro!, simp]:
"k \<in> carrier \<Z>"
@@ -323,8 +324,9 @@
subsection {* Ideals and the Modulus *}
-definition ZMod :: "int => int => int set" where
- "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
+definition
+ ZMod :: "int => int => int set"
+ where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
lemmas ZMod_defs =
ZMod_def genideal_def
@@ -405,8 +407,9 @@
subsection {* Factorization *}
-definition ZFact :: "int \<Rightarrow> int set ring" where
- "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
+definition
+ ZFact :: "int \<Rightarrow> int set ring"
+ where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
lemmas ZFact_defs = ZFact_def FactRing_def