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.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
```