src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 69286 e4d5a07fecb6
parent 69180 922833cc6839
child 69508 2a4c8a2a3f8e
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 14:34:02 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 16:08:59 2018 +0100
     1.3 @@ -761,7 +761,7 @@
     1.4    show ?rhs
     1.5      apply (rule_tac x="s \<inter> t" in exI)
     1.6      using st
     1.7 -    apply (auto simp: Diff_subset holomorphic_on_subset)
     1.8 +    apply (auto simp: holomorphic_on_subset)
     1.9      done
    1.10  next
    1.11    assume ?rhs