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/Cartesian_Euclidean_Space.thy
changeset 53600 8fda7ad57466
parent 53595 5078034ade16
child 54230 b1d955791529 
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 18:09:17 2013 -0700
@@ -499,7 +499,7 @@
   where "matrix f = (\<chi> i j. (f(axis j 1))$i)"
 
 lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
-  by (simp add: linear_def matrix_vector_mult_def vec_eq_iff
+  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
       field_simps setsum_right_distrib setsum_addf)
 
 lemma matrix_works:
isabelle