changeset 7219 | 4e3f386c2e37 |
parent 7127 | 48e235179ffb |
child 9043 | ca761fe227d8 |
7218:bfa767b4dc51 | 7219:4e3f386c2e37 |
---|---|
1 (* Title : Real/RealDef.thy |
1 (* Title : Real/RealDef.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 : The reals |
5 Description : The reals |
5 *) |
6 *) |
6 |
7 |