| changeset 35028 | 108662d50512 |
| parent 32960 | 69916a850301 |
| child 35416 | d8d7d1b785af |
--- a/src/HOL/ZF/Games.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/ZF/Games.thy Fri Feb 05 14:33:50 2010 +0100 @@ -922,7 +922,7 @@ apply (auto simp add: Pg_def quotient_def) done -instance Pg :: pordered_ab_group_add +instance Pg :: ordered_ab_group_add proof fix a b c :: Pg show "a - b = a + (- b)" by (simp add: Pg_diff_def)