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/Determinants.thy
changeset 53600 8fda7ad57466
parent 53253 220f306f5c4e
child 53854 78afb4c4e683 
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Thu Sep 12 18:09:17 2013 -0700
@@ -1080,7 +1080,7 @@
       unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
   note fc = this
   show ?thesis
-    unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
+    unfolding linear_iff vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
     by (simp add: inner_add fc field_simps)
 qed
isabelle