changeset 7219 | 4e3f386c2e37 |
parent 7077 | 60b098bb8b8a |
child 7334 | a90fc1e5fb19 |
7218:bfa767b4dc51 | 7219:4e3f386c2e37 |
---|---|
1 (* Title: Real/Real.thy |
1 (* Title: Real/Real.thy |
2 ID : $Id$ |
|
2 Author: Lawrence C. Paulson |
3 Author: Lawrence C. Paulson |
3 Jacques D. Fleuriot |
4 Jacques D. Fleuriot |
4 Copyright: 1998 University of Cambridge |
5 Copyright: 1998 University of Cambridge |
5 Description: Type "real" is a linear order |
6 Description: Type "real" is a linear order |
6 *) |
7 *) |