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/Multivariate_Analysis/Finite_Cartesian_Product.thy
changeset 54230 b1d955791529
parent 52143 36ffe23b25f8
child 56541 0e3abadbef39 
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -115,7 +115,7 @@
 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
 
 instance vec :: (group_add, finite) group_add
-  by default (simp_all add: vec_eq_iff diff_minus)
+  by default (simp_all add: vec_eq_iff)
 
 instance vec :: (ab_group_add, finite) ab_group_add
   by default (simp_all add: vec_eq_iff)
isabelle