| changeset 23010 | e6b5459f9028 |
| parent 22641 | a5dc96fad632 |
| child 23076 | 1b2acb3ccb29 |
| 23009:01c295dd4a36 | 23010:e6b5459f9028 |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header{* Limits and Continuity (Nonstandard) *} |
8 header{* Limits and Continuity (Nonstandard) *} |
9 |
9 |
10 theory HLim |
10 theory HLim |
11 imports HSEQ Lim |
11 imports Star Lim |
12 begin |
12 begin |
13 |
13 |
14 text{*Nonstandard Definitions*} |
14 text{*Nonstandard Definitions*} |
15 |
15 |
16 definition |
16 definition |