src/HOL/Algebra/Ring.thy

 lemmas finsum_add = add.finprod_mult
 lemmas finsum_infinite = add.finprod_infinite
 
 lemmas finsum_cong = add.finprod_cong
 text \<open>Usually, if this rule causes a failed congruence proof error,
-   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+   the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
    Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
 
 lemmas finsum_reindex = add.finprod_reindex
 
 (* The following would be wrong.  Needed is the equivalent of (^) for addition,

 
 
 subsubsection \<open>Sums over Finite Sets\<close>
 
 lemma (in semiring) finsum_ldistr:
-  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
 proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert x F) then show ?case by (simp add: Pi_def l_distr)
 qed
 
 lemma (in semiring) finsum_rdistr:
-  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
 proof (induct set: finite)
   case empty then show ?case by simp
 next
   case (insert x F) then show ?case by (simp add: Pi_def r_distr)

 subsection \<open>Morphisms\<close>
 
 definition
   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   where "ring_hom R S =
-    {h. h \<in> carrier R -> carrier S &
+    {h. h \<in> carrier R \<rightarrow> carrier S &
       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
         h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^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>}"
 
 lemma ring_hom_memI:

     by (simp add: hom_add [symmetric] R.r_neg S.r_neg del: hom_add)
   with R show ?thesis by simp
 qed
 
 lemma (in ring_hom_cring) hom_finsum [simp]:
-  "f \<in> A -> carrier R ==>
+  "f \<in> A \<rightarrow> carrier R ==>
   h (finsum R f A) = finsum S (h o f) A"
   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
 
 lemma (in ring_hom_cring) hom_finprod:
-  "f \<in> A -> carrier R ==>
+  "f \<in> A \<rightarrow> carrier R ==>
   h (finprod R f A) = finprod S (h o f) A"
   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
 
 declare ring_hom_cring.hom_finprod [simp]