--- a/src/ZF/ex/Ring.thy Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Ring.thy Tue Mar 06 16:46:27 2012 +0000
@@ -115,13 +115,13 @@
lemma (in abelian_group) a_l_cancel [simp]:
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
- \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
+ \<Longrightarrow> (x \<oplus> y = x \<oplus> z) \<longleftrightarrow> (y = z)"
by (rule group.l_cancel [OF a_group,
simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_group) a_r_cancel [simp]:
"\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
- \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
+ \<Longrightarrow> (y \<oplus> x = z \<oplus> x) \<longleftrightarrow> (y = z)"
by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
lemma (in abelian_monoid) a_assoc:
@@ -234,7 +234,7 @@
ring_hom :: "[i,i] => i" where
"ring_hom(R,S) ==
{h \<in> carrier(R) -> carrier(S).
- (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
+ (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) \<longrightarrow>
h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"