Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Multivariate_Analysis/L2_Norm.thy
changeset 41891 d37babdf5cae
parent 36333 82356c9e218a
child 41959 b460124855b8 
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Thu Mar 03 18:43:15 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Thu Mar 03 21:43:06 2011 +0100
@@ -44,7 +44,7 @@
   assumes "\<And>i. i \<in> K \<Longrightarrow> 0 \<le> f i"
   shows "setL2 f K \<le> setL2 g K"
   unfolding setL2_def
-  by (simp add: setsum_nonneg setsum_mono power_mono prems)
+  by (simp add: setsum_nonneg setsum_mono power_mono assms)
 
 lemma setL2_strict_mono:
   assumes "finite K" and "K \<noteq> {}"
isabelle