Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Power.thy
changeset 25231 1aa9c8f022d0
parent 25162 ad4d5365d9d8
child 25836 f7771e4f7064 
--- 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]:
isabelle