equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Frechet Derivative *} |
5 header {* Frechet Derivative *} |
6 |
6 |
7 theory FrechetDeriv |
7 theory FrechetDeriv |
8 imports Complex_Main |
8 imports "~~/src/HOL/Complex_Main" |
9 begin |
9 begin |
10 |
10 |
11 definition |
11 definition |
12 fderiv :: |
12 fderiv :: |
13 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |
13 "['a::real_normed_vector \<Rightarrow> 'b::real_normed_vector, 'a, 'a \<Rightarrow> 'b] \<Rightarrow> bool" |