| changeset 52265 | bb907eba5902 |
| parent 51642 | 400ec5ae7f8f |
| child 53381 | 355a4cac5440 |
| 52264:cdba0c3cb4c2 | 52265:bb907eba5902 |
|---|---|
1 (* Title: Limits.thy |
1 (* Title: HOL/Limits.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 Author: Jacques D. Fleuriot, University of Cambridge |
3 Author: Jacques D. Fleuriot, University of Cambridge |
4 Author: Lawrence C Paulson |
4 Author: Lawrence C Paulson |
5 Author: Jeremy Avigad |
5 Author: Jeremy Avigad |
6 |
6 |