changeset 7219 | 4e3f386c2e37 |
parent 5078 | 7b5ea59c0275 |
child 7292 | dff3470c5c62 |
7218:bfa767b4dc51 | 7219:4e3f386c2e37 |
---|---|
1 (* Title : RComplete.thy |
1 (* Title : RComplete.thy |
2 ID : $Id$ |
|
2 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
4 Description : Completeness theorems for positive |
5 Description : Completeness theorems for positive |
5 reals and reals |
6 reals and reals |
6 *) |
7 *) |