--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Nov 14 12:42:06 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Nov 14 13:48:36 2019 +0100
@@ -79,7 +79,7 @@
lemma content_pos_le [iff]: "0 \<le> content X"
by simp
-corollary content_nonneg [simp]: "\<not> content (cbox a b) < 0"
+corollary\<^marker>\<open>tag unimportant\<close> content_nonneg [simp]: "\<not> content (cbox a b) < 0"
using not_le by blast
lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Nov 14 12:42:06 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Nov 14 13:48:36 2019 +0100
@@ -698,10 +698,10 @@
lemmas independent_imp_finite = finiteI_independent
-corollary
+corollary\<^marker>\<open>tag unimportant\<close> independent_card_le:
fixes S :: "'a::euclidean_space set"
assumes "independent S"
- shows independent_card_le:"card S \<le> DIM('a)"
+ shows "card S \<le> DIM('a)"
using assms independent_bound by auto
lemma dependent_biggerset: