# HG changeset patch
# User haftmann
# Date 1193730355 -3600
# Node ID 1aa9c8f022d00d55d4cf415b39eb54582a255cd7
# Parent  022029099a83e5eaa562e7eabe173abb771617a5
simplified proof

diff -r 022029099a83 -r 1aa9c8f022d0 src/HOL/Nat.thy
--- 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)))"
diff -r 022029099a83 -r 1aa9c8f022d0 src/HOL/Power.thy
--- 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]: