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/Analysis/Linear_Algebra.thy
changeset 66641 ff2e0115fea4
parent 66503 7685861f337d
child 66804 3f9bb52082c4 
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 11:09:56 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 08 12:49:40 2017 +0100
@@ -310,7 +310,7 @@
 lemma span_minimal: "S \<subseteq> T \<Longrightarrow> subspace T \<Longrightarrow> span S \<subseteq> T"
   unfolding span_def by (rule hull_minimal)
 
-lemma span_UNIV: "span UNIV = UNIV"
+lemma span_UNIV [simp]: "span UNIV = UNIV"
   by (intro span_unique) auto
 
 lemma (in real_vector) span_induct:
isabelle