# HG changeset patch
# User wenzelm
# Date 1573744941 -3600
# Node ID 3e61534e804e9310598247aef890e3bfd8339079
# Parent  8d51418d4ec02a4ef42d82b18bc6bd3276c15bbd# Parent  557703db74c33e3c39a2e11c5deae8e2717c3b9d
merged

diff -r 557703db74c3 -r 3e61534e804e src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Nov 14 16:22:04 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Nov 14 16:22:21 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)"
diff -r 557703db74c3 -r 3e61534e804e src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Nov 14 16:22:04 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Nov 14 16:22:21 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: