# HG changeset patch
# User huffman
# Date 1379002006 25200
# Node ID 5078034ade163a151be6c38f262b7dd5091d3366
# Parent  8a9fb53294f4aa40be8eb9238bb4a8194416571a
prefer theorem name over 'long_thm_list(n)'

diff -r 8a9fb53294f4 -r 5078034ade16 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 09:04:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 09:06:46 2013 -0700
@@ -291,7 +291,7 @@
   by (metis component_le_norm_cart order_trans)
 
 lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e"
-  by (metis component_le_norm_cart basic_trans_rules(21))
+  by (metis component_le_norm_cart le_less_trans)
 
 lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def setL2_le_setsum)
diff -r 8a9fb53294f4 -r 5078034ade16 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 12 09:04:46 2013 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Sep 12 09:06:46 2013 -0700
@@ -1521,7 +1521,7 @@
   by (metis Basis_le_norm order_trans)
 
 lemma norm_bound_Basis_lt: "b \<in> Basis \<Longrightarrow> norm x < e \<Longrightarrow> \<bar>x \<bullet> b\<bar> < e"
-  by (metis Basis_le_norm basic_trans_rules(21))
+  by (metis Basis_le_norm le_less_trans)
 
 lemma norm_le_l1: "norm x \<le> (\<Sum>b\<in>Basis. \<bar>x \<bullet> b\<bar>)"
   apply (subst euclidean_representation[of x, symmetric])