src/HOL/OrderedGroup.thy
changeset 25102 db3e412c4cb1
parent 25090 4a50b958391a
child 25194 37a1743f0fc3
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Oct 19 16:20:27 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Oct 19 19:45:29 2007 +0200
     1.3 @@ -879,7 +879,7 @@
     1.4    then have "a + a + - a = - a" by simp
     1.5    then have "a + (a + - a) = - a" by (simp only: add_assoc)
     1.6    then have a: "- a = a" by simp (*FIXME tune proof*)
     1.7 -  show "a = 0" apply rule
     1.8 +  show "a = 0" apply (rule antisym)
     1.9    apply (unfold neg_le_iff_le [symmetric, of a])
    1.10    unfolding a apply simp
    1.11    unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]