| changeset 51525 | d3d170a2887f |
| parent 50322 | b06b95a5fda2 |
| child 54230 | b1d955791529 |
| 51524:7cb5ac44ca9e | 51525:d3d170a2887f |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header{* Limits and Continuity (Nonstandard) *} |
6 header{* Limits and Continuity (Nonstandard) *} |
7 |
7 |
8 theory HLim |
8 theory HLim |
9 imports Star Lim |
9 imports Star |
10 begin |
10 begin |
11 |
11 |
12 text{*Nonstandard Definitions*} |
12 text{*Nonstandard Definitions*} |
13 |
13 |
14 definition |
14 definition |