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/Library/Parity.thy
changeset 25162 ad4d5365d9d8
parent 25134 3d4953e88449
child 25502 9200b36280c0 
--- a/src/HOL/Library/Parity.thy	Tue Oct 23 22:48:25 2007 +0200
+++ b/src/HOL/Library/Parity.thy	Tue Oct 23 23:27:23 2007 +0200
@@ -222,7 +222,7 @@
   apply (subst power_add)
   apply (subst zero_le_mult_iff)
   apply auto
-  apply (subgoal_tac "x = 0 & y \<noteq> 0")
+  apply (subgoal_tac "x = 0 & y > 0")
   apply (erule conjE, assumption)
   apply (subst power_eq_0_iff [symmetric])
   apply (subgoal_tac "0 <= x^y * x^y")
isabelle