| changeset 32437 | 66f1a0dfe7d9 |
| parent 32436 | 10cd49e0c067 |
| child 32642 | 026e7c6a6d08 |
--- a/src/HOL/OrderedGroup.thy Fri Aug 28 18:52:41 2009 +0200 +++ b/src/HOL/OrderedGroup.thy Fri Aug 28 19:15:59 2009 +0200 @@ -1275,7 +1275,7 @@ proof - note add_le_cancel_right [of a a "- a", symmetric, simplified] moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified] - then show ?thesis by (auto simp: sup_max max_def) + then show ?thesis by (auto simp: sup_max) qed lemma abs_if_lattice: