--- a/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jul 04 20:18:47 2014 +0200
@@ -53,7 +53,7 @@
proof (cases "m\<ge>n")
have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
case True
- then obtain k where *:"m = k + n" and **:"m = n + k" by (metis Nat.le_iff_add nat_add_commute)
+ then obtain k where *:"m = k + n" and **:"m = n + k" by (metis Nat.le_iff_add add.commute)
have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = a (^) k"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc)
also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
@@ -63,7 +63,7 @@
have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
case False
then obtain k where *:"n = k + m" and **:"n = m + k"
- by (metis Nat.le_iff_add nat_add_commute nat_le_linear)
+ by (metis Nat.le_iff_add add.commute nat_le_linear)
have "a (^) (m::nat) \<otimes> inv (a (^) (n::nat)) = inv(a (^) k)"
using * by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)
also have "\<dots> = inv (a (^) n) \<otimes> a (^) m"
@@ -86,7 +86,7 @@
proof(cases "b\<ge>c")
have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
case True
- then obtain n where "b = n + c" by (metis Nat.le_iff_add nat_add_commute)
+ then obtain n where "b = n + c" by (metis Nat.le_iff_add add.commute)
then have "d = n + e" using eq by arith
from `b = _` have "a (^) b \<otimes> inv (a (^) c) = a (^) n"
by (auto simp add: nat_pow_mult[symmetric] m_assoc)
@@ -96,7 +96,7 @@
next
have [simp]: "a \<in> carrier G" using `a \<in> _` by (rule Units_closed)
case False
- then obtain n where "c = n + b" by (metis Nat.le_iff_add nat_add_commute nat_le_linear)
+ then obtain n where "c = n + b" by (metis Nat.le_iff_add add.commute nat_le_linear)
then have "e = n + d" using eq by arith
from `c = _` have "a (^) b \<otimes> inv (a (^) c) = inv (a (^) n)"
by (auto simp add: nat_pow_mult[symmetric] m_assoc[symmetric] inv_mult_units)