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/Library/Product_Vector.thy
changeset 56536 aefb4a8da31f
parent 56381 0556204bc230
child 56541 0e3abadbef39 
--- a/src/HOL/Library/Product_Vector.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -446,7 +446,6 @@
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
 apply (simp add: power2_sum x y)
-apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done
isabelle