Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prefer theorem name over 'long_thm_list(n)'
authorhuffman
Thu, 12 Sep 2013 09:06:46 -0700
changeset 53595 5078034ade16
parent 53594 8a9fb53294f4
child 53596 d29d63460d84
prefer theorem name over 'long_thm_list(n)'
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy file | annotate | diff | comparison | revisions
src/HOL/Multivariate_Analysis/Linear_Algebra.thy file | annotate | diff | comparison | revisions 
--- 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)
--- 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])
isabelle