simplified proof
authorhaftmann
Tue Oct 30 08:45:55 2007 +0100 (2007-10-30)
changeset 252311aa9c8f022d0
parent 25230 022029099a83
child 25232 9b4d0c13c332
simplified proof
src/HOL/Nat.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Nat.thy	Tue Oct 30 08:45:54 2007 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Oct 30 08:45:55 2007 +0100
     1.3 @@ -1289,7 +1289,7 @@
     1.4  end
     1.5  
     1.6  lemma abs_of_nat [simp]: "\<bar>of_nat n::'a::ordered_idom\<bar> = of_nat n"
     1.7 -  by (rule of_nat_0_le_iff [THEN abs_of_nonneg])
     1.8 +  unfolding abs_if by auto
     1.9  
    1.10  lemma nat_diff_split_asm:
    1.11    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
     2.1 --- a/src/HOL/Power.thy	Tue Oct 30 08:45:54 2007 +0100
     2.2 +++ b/src/HOL/Power.thy	Tue Oct 30 08:45:55 2007 +0100
     2.3 @@ -194,7 +194,8 @@
     2.4      show ?case by (simp add: zero_less_one)
     2.5  next
     2.6    case (Suc n)
     2.7 -    show ?case by (force simp add: prems power_Suc zero_less_mult_iff)
     2.8 +    show ?case by (auto simp add: prems power_Suc zero_less_mult_iff
     2.9 +      abs_zero)
    2.10  qed
    2.11  
    2.12  lemma zero_le_power_abs [simp]: