src/HOL/Modules.thy

--- a/src/HOL/Modules.thy	Thu May 03 15:07:14 2018 +0200
+++ b/src/HOL/Modules.thy	Thu May 03 16:17:44 2018 +0200
@@ -186,7 +186,7 @@
 lemma span_zero: "0 \<in> span S"
   by (auto simp: span_explicit intro!: exI[of _ "{}"])
 
-lemma span_UNIV: "span UNIV = UNIV"
+lemma span_UNIV[simp]: "span UNIV = UNIV"
   by (auto intro: span_base)
 
 lemma span_add: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x + y \<in> span S"