src/HOL/Algebra/Ring.thy
changeset 67341 df79ef3b3a41
parent 67091 1393c2340eec
child 67398 5eb932e604a2
     1.1 --- a/src/HOL/Algebra/Ring.thy	Fri Jan 05 15:24:57 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Ring.thy	Fri Jan 05 18:41:42 2018 +0100
     1.3 @@ -146,13 +146,13 @@
     1.4  
     1.5  lemmas finsum_reindex = add.finprod_reindex
     1.6  
     1.7 -(* The following would be wrong.  Needed is the equivalent of (^) for addition,
     1.8 +(* The following would be wrong.  Needed is the equivalent of [^] for addition,
     1.9    or indeed the canonical embedding from Nat into the monoid.
    1.10  
    1.11  lemma finsum_const:
    1.12    assumes fin [simp]: "finite A"
    1.13        and a [simp]: "a : carrier G"
    1.14 -    shows "finsum G (%x. a) A = a (^) card A"
    1.15 +    shows "finsum G (%x. a) A = a [^] card A"
    1.16    using fin apply induct
    1.17    apply force
    1.18    apply (subst finsum_insert)
    1.19 @@ -427,7 +427,7 @@
    1.20    a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
    1.21  
    1.22  lemma (in semiring) nat_pow_zero:
    1.23 -  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> (^) n = \<zero>"
    1.24 +  "(n::nat) \<noteq> 0 \<Longrightarrow> \<zero> [^] n = \<zero>"
    1.25    by (induct n) simp_all
    1.26  
    1.27  context semiring begin