| changeset 41959 | b460124855b8 |
| parent 41589 | bbd861837ebc |
| child 50249 | 3f0920f8a24e |
| 41958:5abc60a017e0 | 41959:b460124855b8 |
|---|---|
1 (* Title: HLim.thy |
1 (* Title: HOL/NSA/HLim.thy |
2 Author: Jacques D. Fleuriot, University of Cambridge |
2 Author: Jacques D. Fleuriot, University of Cambridge |
3 Author: Lawrence C Paulson |
3 Author: Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header{* Limits and Continuity (Nonstandard) *} |
6 header{* Limits and Continuity (Nonstandard) *} |