# HG changeset patch
# User immler
# Date 1547765401 18000
# Node ID 94284d4dab987b0a3048c36f1c74842bc7d62b65
# Parent  8b3458ca076286051dd195056aaba53789a2efa2
amending 689997a8a582

diff -r 8b3458ca0762 -r 94284d4dab98 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 16:38:00 2019 -0500
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Jan 17 17:50:01 2019 -0500
@@ -626,7 +626,7 @@
 lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def L2_set_le_sum)
 
-lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)"
 apply standard
 apply (rule vector_add_component)
 apply (rule vector_scaleR_component)