--- a/src/HOL/Nat.thy Tue Oct 30 08:45:54 2007 +0100
+++ b/src/HOL/Nat.thy Tue Oct 30 08:45:55 2007 +0100
@@ -1289,7 +1289,7 @@
end
lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
- by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
+ unfolding abs_if by auto
lemma nat_diff_split_asm:
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
--- a/src/HOL/Power.thy Tue Oct 30 08:45:54 2007 +0100
+++ b/src/HOL/Power.thy Tue Oct 30 08:45:55 2007 +0100
@@ -194,7 +194,8 @@
show ?case by (simp add: zero_less_one)
next
case (Suc n)
- show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
+ show ?case by (auto simp add: prems power_Suc zero_less_mult_iff
+ abs_zero)
qed
lemma zero_le_power_abs [simp]: