| changeset 29197 | 6d4cb27ed19c |
| parent 28952 | 15a4b2cf8c34 |
| child 29667 | 53103fc8ffa3 |
| 29189:ee8572f3bb57 | 29197:6d4cb27ed19c |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header{* Limits and Continuity *} |
7 header{* Limits and Continuity *} |
8 |
8 |
9 theory Lim |
9 theory Lim |
10 imports "~~/src/HOL/Hyperreal/SEQ" |
10 imports SEQ |
11 begin |
11 begin |
12 |
12 |
13 text{*Standard Definitions*} |
13 text{*Standard Definitions*} |
14 |
14 |
15 definition |
15 definition |