equal
deleted
inserted
replaced
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
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 = CSeries: |
9 theory CLim |
|
10 import CSeries |
|
11 begin |
10 |
12 |
11 (*not in simpset?*) |
13 (*not in simpset?*) |
12 declare hypreal_epsilon_not_zero [simp] |
14 declare hypreal_epsilon_not_zero [simp] |
13 |
15 |
14 (*??generalize*) |
16 (*??generalize*) |