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/Inner_Product.thy
changeset 56381 0556204bc230
parent 56181 2aa0b19e74f3
child 57512 cc97b347b301 
--- a/src/HOL/Library/Inner_Product.thy	Thu Apr 03 17:16:02 2014 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Thu Apr 03 17:56:08 2014 +0200
@@ -180,7 +180,7 @@
 lemmas isCont_inner [simp] =
   bounded_bilinear.isCont [OF bounded_bilinear_inner]
 
-lemmas has_derivative_inner [has_derivative_intros] =
+lemmas has_derivative_inner [derivative_intros] =
   bounded_bilinear.FDERIV [OF bounded_bilinear_inner]
 
 lemmas bounded_linear_inner_left =
@@ -189,10 +189,10 @@
 lemmas bounded_linear_inner_right =
   bounded_bilinear.bounded_linear_right [OF bounded_bilinear_inner]
 
-lemmas has_derivative_inner_right [has_derivative_intros] =
+lemmas has_derivative_inner_right [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_inner_right]
 
-lemmas has_derivative_inner_left [has_derivative_intros] =
+lemmas has_derivative_inner_left [derivative_intros] =
   bounded_linear.has_derivative [OF bounded_linear_inner_left]
 
 lemma differentiable_inner [simp]:
isabelle