author | wenzelm |
Wed, 10 May 2000 22:34:30 +0200 | |
changeset 8856 | 435187ffc64e |
parent 7334 | a90fc1e5fb19 |
child 10797 | 028d22926a41 |
permissions | -rw-r--r-- |
7292 | 1 |
(* Title: RealInt.thy |
2 |
ID: $Id$ |
|
3 |
Author: Jacques D. Fleuriot |
|
4 |
Copyright: 1999 University of Edinburgh |
|
5 |
Description: Embedding the integers in the reals |
|
6 |
*) |
|
7 |
||
8856 | 8 |
RealInt = RealOrd + |
7292 | 9 |
|
10 |
constdefs |
|
11 |
real_of_int :: int => real |
|
12 |
"real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ |
|
13 |
{(preal_of_prat(prat_of_pnat(pnat_of_nat i)), |
|
14 |
preal_of_prat(prat_of_pnat(pnat_of_nat j)))})" |
|
15 |
||
16 |
||
17 |
end |