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/OrderedGroup.thy
changeset 25102 db3e412c4cb1
parent 25090 4a50b958391a
child 25194 37a1743f0fc3 
--- a/src/HOL/OrderedGroup.thy	Fri Oct 19 16:20:27 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Oct 19 19:45:29 2007 +0200
@@ -879,7 +879,7 @@
   then have "a + a + - a = - a" by simp
   then have "a + (a + - a) = - a" by (simp only: add_assoc)
   then have a: "- a = a" by simp (*FIXME tune proof*)
-  show "a = 0" apply rule
+  show "a = 0" apply (rule antisym)
   apply (unfold neg_le_iff_le [symmetric, of a])
   unfolding a apply simp
   unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
isabelle