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/Complex_Analysis_Basics.thy
changeset 62540 f2fc5485e3b0
parent 62534 6855b348e828
child 63092 a949b2a5f51d 
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Mar 09 17:16:08 2016 +0000
@@ -443,7 +443,7 @@
     "f holomorphic_on s \<Longrightarrow> continuous_on s f"
   by (metis field_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def)
 
-lemma holomorphic_on_subset:
+lemma holomorphic_on_subset [elim]:
     "f holomorphic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f holomorphic_on t"
   unfolding holomorphic_on_def
   by (metis field_differentiable_within_subset subsetD)
isabelle