src/HOL/Power.thy
 changeset 57512 cc97b347b301 parent 57418 6ab1c7cb0b8d child 57514 bdc2c6b40bf2
```--- a/src/HOL/Power.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Power.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -53,7 +53,7 @@

lemma power_commutes:
"a ^ n * a = a * a ^ n"
-  by (induct n) (simp_all add: mult_assoc)
+  by (induct n) (simp_all add: mult.assoc)

lemma power_Suc2:
"a ^ Suc n = a ^ n * a"
@@ -71,11 +71,11 @@

lemma power3_eq_cube: "a ^ 3 = a * a * a"
-  by (simp add: numeral_3_eq_3 mult_assoc)
+  by (simp add: numeral_3_eq_3 mult.assoc)

lemma power_even_eq:
"a ^ (2 * n) = (a ^ n)\<^sup>2"
-  by (subst mult_commute) (simp add: power_mult)
+  by (subst mult.commute) (simp add: power_mult)

lemma power_odd_eq:
"a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
@@ -88,7 +88,7 @@
lemma power_numeral_odd:
"z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
-  unfolding power_Suc power_add Let_def mult_assoc ..
+  unfolding power_Suc power_add Let_def mult.assoc ..

lemma funpow_times_power:
"(times x ^^ f x) = times (x ^ f x)"
@@ -100,7 +100,7 @@
with Suc have "n = g x" by simp
with Suc have "times x ^^ g x = times (x ^ g x)" by simp
moreover from Suc g_def have "f x = g x + 1" by simp
qed

end
@@ -197,7 +197,7 @@
case 0 show ?case by simp
next
case (Suc n) then show ?case
-    by (simp del: power_Suc add: power_Suc2 mult_assoc)
+    by (simp del: power_Suc add: power_Suc2 mult.assoc)
qed

lemma power_minus_Bit0:
@@ -626,7 +626,7 @@
lemma power2_diff:
fixes x y :: "'a::comm_ring_1"
shows "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
-  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute)
+  by (simp add: ring_distribs power2_eq_square mult_2) (rule mult.commute)

lemma power_0_Suc [simp]:
"(0::'a::{power, semiring_0}) ^ Suc n = 0"```