| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15228 | 4d332d10fa3d |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header{*Limits, Continuity and Differentiation for Complex Functions*} |
7 header{*Limits, Continuity and Differentiation for Complex Functions*} |
8 |
8 |
9 theory CLim |
9 theory CLim |
10 import CSeries |
10 imports CSeries |
11 begin |
11 begin |
12 |
12 |
13 (*not in simpset?*) |
13 (*not in simpset?*) |
14 declare hypreal_epsilon_not_zero [simp] |
14 declare hypreal_epsilon_not_zero [simp] |
15 |
15 |