src/HOL/Library/Product_plus.thy
changeset 54230 b1d955791529
parent 51301 6822aa82aafa
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Product_plus.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Product_plus.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4    (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
     1.5  
     1.6  instance prod :: (group_add, group_add) group_add
     1.7 -  by default (simp_all add: prod_eq_iff diff_minus)
     1.8 +  by default (simp_all add: prod_eq_iff)
     1.9  
    1.10  instance prod :: (ab_group_add, ab_group_add) ab_group_add
    1.11    by default (simp_all add: prod_eq_iff)