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